package frama-clang
Elements of specification generated from the C++ conversion itself.
val add_contract :
env:Convert_env.env ->
kind:Intermediate_format.funkind ->
return_type:Intermediate_format.qual_type ->
args:Intermediate_format.arg_decl list ->
variadic:bool ->
implicit:bool ->
extern_c:bool ->
(Frama_c_kernel.Logic_ptree.spec * Frama_c_kernel.Cabs.cabsloc) option ->
(Frama_c_kernel.Logic_ptree.spec * Frama_c_kernel.Cabs.cabsloc) option
adds contract elements to the default behavior of the given spec related to the corresponding signature elements.
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>