tests/spec · 6b0ea8378fcebcaec7b9ec0aa185d8767b101feb · pub / frama-c

[Kernel] Adapt Infer_annotations to ghost parameters.

Allan Blanchard authored 5 years ago

Assume that ghost parameters are well-typed.

6b0ea837

History

6b0ea837 5 years ago

History

Name	Last commit	Last update
..
oracle
Extend.i
Extend.ml
Type_of_term.ml
_Bool.i
abrupt.i
acsl_allocator.c
acsl_basic_allocator.c
acsl_by_example.c
add_global.i
add_global.ml
all.c
alloc_string_marshall.c
allocates.i
annot_decl_bts1009.i
annot_main.c
array_conversion.c
array_prm.c
array_typedef.c
assert_label.i
assign_in_spec.c
assignable_location.i
assigns.c
assigns_array.c
assigns_from_kf.i
assigns_from_kf.ml
assigns_result.i
assigns_void.c
assume.c
at.c
at_exit.c
axiom_ignored_bts1116.i
axiom_included.c
axiom_included.h
axiom_included_1.c
axiom_redef_bts1005.i
behavior_assert.c
behavior_names.c
behaviors_decl_def.c
bool.c
boolean_ops.c
breaks_continues_unroll.i
bsearch.c
bts0254.i
bts0283.c
bts0440.i
bts0549.i
bts0570.i
bts0578.i
bts0578.ml
bts0589.i
bts0655.i
bts0655.ml
bts0698.i
bts0812.c
bts1068.i
bts1262.c
bts2187-no-empty-contract.i
bts_1789.i
bug96.c
builtins.c
cast_enum_bts1546.i
char_cst.c
clash_double_file_bts1598.c
comparison.i
comparison.ml
complete_behaviors.c
concrete_type.c
conf1.h
const.c
const_ptr_bts1729.i
constant_predicate.i
contract_assert_bts1470.i
conversion.c
dec.h
declspec.c
default_assigns_bts0966.i
doxygen.c
enum.c
error_msg.i
exit_clause.c
expr_to_term.i
expr_to_term.ml
fct_ptr.c
first.c
float-acsl.i
footprint.c
for_scope.c
fptr.i
ghost.c
global_invariant.c
heterogeneous_set_bts1146.i
homax.c
hosum.c
if.c
kw.c
label_scope_bts1536.i
lib.c
lib.h
liens.c
list.i
local.c
localization.c
location_char.c
location_char.ml
logic_array.i
logic_coerce.i
logic_compare.c
logic_def.c
logic_label.c
logic_labels_wrong.c
logic_type.c
loop_labels.i
loop_labels_unroll.i
max.c
merge_1.i
merge_2.i
merge_assigns_bts1253.i
merge_bts938.c
merge_bts938.h
merge_bts938_1.c
merge_different_assigns.i
merge_different_assigns_bis.i
merge_logic_globals.h
merge_logic_globals_1.c
merge_logic_globals_2.c
model.i
model.ml
model1.c
model1.h
model2.c
multi_axiomatic_1.i
multi_axiomatic_2.i
multi_behavior.c
multi_labels.i
multidecl.c
multidim.c
multiple_decl_def_1.c
multiple_decl_def_2.c
multiple_file_1.c
multiple_file_2.c
multiple_include.h
multiple_include_1.c
multiple_include_2.c
multiple_spec.c
nested.c
null_ptr.c
old_prm.i
onelineghost.c
overload_resolution.i
parsing.c
permut.c
pi.c
pointer_cast.c
pointer_comparable.c
polymorph.c
pp_empty_spec.i
pp_empty_spec.ml
pragma.i
prec_i.h
precedence.i
pred_def.i
predicates.c
preprocess.c
preprocess.h
preprocess_string.c
printf_assigns.c
property_test.i
property_test.ml
prototype_assigns.c
ptr_cast.c
purse.c
range.c
real_typing_bts1309.i
recursive_with_label.i
regions.c
regions2.c
reset_env.i
returns.i
second.c
separated.c
shifts.c
sizeof.c
sizeof_incomplete_bts1538.i
sizeof_logic.i
source_annot.c
spec_zero_arg.c
statement_behavior.c
stmt_contract.i
string.c
struct_invariant.c
tableau_zones.c
temporal.i
terminates.c
test_config
third.c
transitive_rel.c
tsets.c
type_constructors_in_env.i
type_constructors_in_env.ml