tests/value · 5d48c248010dd58ed3072e0b3cf6adacb8ee6dcf · pub / frama-c

[Eva] Emits alarms on a%b when a/b overflows.

David Bühler authored 6 months ago

According to the C standard, section 6.5.5 §6:
"If the quotient a/b is representable, the expression (a/b)*b + a%b shall equal a;
otherwise, the behavior of both a/b and a%b is undefined."

5d48c248

History

5d48c248 6 months ago

History

Name	Last commit	Last update
..
numerors
oracle
oracle_apron
oracle_bitwise
oracle_equality
oracle_gauges
oracle_multidim
oracle_octagon
oracle_symblocs
traces
.gitignore
CruiseControl.c
CruiseControl.h
CruiseControl_const.c
CruiseControl_extern.h
FP5.i
abs.i
abs_addr.i
absolute_pointer.c
abstract_struct_1.c
abstract_struct_2.c
access_path.i
add_approx.i
addition.i
addr.i
addr2.i
addrofstring.c
affect_corrupt.i
ai_annot.i
alias.i
align.i
align_char_array.c
annot.i
annot_valid.i
anonymous_field.i
any_int.c
arch.i
arg_array.i
arith_pointer.c
array_access.c
array_array.c
array_bounds.i
array_degenerating_loop.i
array_initializer.i
array_loop.i
array_overlap.i
array_ptr.i
array_zero_length.i
asm_contracts.c
assert_ptr.i
assign-leaf-indirect.i
assigns.i
assigns_from.i
assigns_from_direct.i
attribute-aligned.c
auto_loop_unroll.c
automalloc.i
backward_add_ptr.c
backward_arith.i
bad_loop.i
base_addr_offset_block_length.i
behavior_statuses.i
behaviors1.i
behaviors2.c
big_lib_entry.i
bigarray.c
bitfield.i
bitfield_assign.i
bitfield_longlong.c
bitfield_receives_result.i
bitwise.i
bitwise_float.c
bitwise_pointer.i
bitwise_reduction.i
biz.i
bool.i
branch.i
branch2.i
broken_loop.i
bts0506.i
bts0775.i
bts0858.i
bts1306.i
buffer_overflow.i
bug.i
bug0196.c
bug0223.i
bug0245.i
bug_023.i
bug_0244.i
builtins_split.c
call.i
call_2.i
call_3.i
call_alias.i
call_deep.i
call_multi.i
call_simple.i
calls_annotation.i
case_analysis.i
cast.i
cast1.i
cast2.i
cast_axalto.c
cast_fun.i
cast_hetero.i
cast_return.c
cert_exp35_c.i
changeret.i
cmp.i
cmp_ptr.i
cmp_ptr_follow_all_branches.i
cond.i
cond2.i
cond_integer_cast_of_float.i
conditional_initializer.i
config.h
config_types.h
const.i
const2.i
const_syntax.i
const_typedef.i
constarraystructlibentry.i
context_free.i
context_free_simple.i
context_width.i
control.i
conversion.i
copy_paste.i
copy_paste_hidden_by_dummy_cast.i
copy_stdin.i
dangling.i
dataflow_order.i
dead_code.i
dead_code2.i
dead_inout.i
dead_statuses.i
deep_conditionals.i
definitions.h
degeneration2.i
deps.i
deps_addr.i
deps_compose.i
deps_local.i
deps_mixed.i
deps_unitialized_locals.i
deref.i
descending.i
disjoint_status.i
div.i
div_strange.i
divneg.i
domains.i
domains_function.c
downcast.i
duff.i
dur.i
empty_struct.c
empty_struct2.c
empty_union.c
endian.i
enum.i
enum2.c
equality.c
eval_separated.c
exit_paths.i
extern.i
f1.i
f2.i
false.i
fam_sizeof.i
find_ivaltop.i
folding.i
for_loops.c
forall.i
fptr.i
from1.i
from_call.i
from_global.i
from_ind.i
from_pb.i
from_ptr.i
from_ptr2.i
from_res_2.i
from_termin.i
fun_ptr.i
function_return_serial_casts.i
g1.i
garbled_init.c
gauges.c
ghost.i
global_bug.i
goto.i
hierarchical_convergence.c
if.i
if2.i
ilevel.c
implies.i
imprecise_invalid_write.i
incompatible_states.c