Skip to content
Snippets Groups Projects
Commit 41235626 authored by Andre Maroneze's avatar Andre Maroneze
Browse files

[Value] new str* builtins

parent d825c057
No related branches found
No related tags found
No related merge requests found
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 8007 additions and 945 deletions
src/plugins/value/builtins_nonfree.ml
+ 0
− 708
View file @ 41235626
......@@ -24,8 +24,6 @@ let dkey = Value_parameters.register_category "imprecision"
exception Base_aligned_error
exception Found_misaligned_base
let two61 = Integer.two_power_of_int 61
let frama_C_is_base_aligned state actuals =
try begin
match actuals with
......@@ -728,712 +726,6 @@ let frama_c_memset state actuals =
let () = register_builtin "Frama_C_memset" frama_c_memset
(* strlen builtin *)
exception Abort_to_top
let is_init v =
Cvalue.V_Or_Uninitialized.is_initialized v
let singleton_eight = Ival.inject_singleton Int.eight
let abstract_strlen ~max ~emit_alarm str state =
(* Checks whether the call to strlen would provoke a rte:
Calls emit_alarm (e.g. to emit \valid_string(...)) if anything at all
is wrong.
Returns top_int in most complicated cases
(e.g. too many offsets to consider)
*)
Value_parameters.debug "string offsetmap is %a"
Location_Bytes.pretty str ;
let with_alarms =
let emit = { CilE.a_log = false; CilE.a_call = emit_alarm } in
{ CilE.imprecision_tracing = CilE.a_ignore;
defined_logic = emit;
unspecified = emit;
others = emit;
}
in
let value =
try
match str with
| Location_Bytes.Top(_,_) ->
emit_alarm();
Ival.top
| Location_Bytes.Map m ->
let do_one_offsetmap base ival =
(* The right way to do it would be:
start from min of ival,
accumulate and do some work when crossing start of next ival value.
If bottoming, start again from next ival value.
The current implementation has subpar complexity (Ival.fold_enum).
*)
Value_parameters.debug "Base %a" Base.pretty base;
Value_parameters.debug "Ival is %a" Ival.pretty ival ;
let validity = Base.validity base in
match Cvalue.Model.find_base_or_default base state with
| `Bottom -> Ival.bottom
| `Top -> raise Abort_to_top
| `Map offsetmap ->
Value_parameters.debug "omap is %a"
Cvalue.V_Offsetmap.pretty offsetmap;
let val_strlen =
Ival.fold_enum
(* does nothing for ival *)
(fun ival acc_val ->
let rival = ref (Ival.scale Int.eight ival) in
let offset = ref Int.zero in
let continue = ref true in
let racc = ref acc_val in
while !continue && Int.lt !offset max do
let alarm, v =
Cvalue.V_Offsetmap.find
~validity ~offsets:!rival ~size:Int.eight offsetmap
in
if alarm then Valarms.warn_mem_read with_alarms;
Value_parameters.debug "find_ival(8) on %a returns %a"
Ival.pretty !rival
Cvalue.V_Or_Uninitialized.pretty v ;
if not (is_init v) then
begin
Value_parameters.debug "Uninitialized: end of string" ;
racc :=
Ival.join !racc
(Ival.inject_singleton !offset)
end
else
begin
let v' = Cvalue.V_Or_Uninitialized.get_v v in
if Cvalue.V.is_bottom v' then (
continue := false ;
Value_parameters.debug
"continue set to false because invalid address"
)
else (
let iv =
try
V.project_ival v'
with V.Not_based_on_null ->
Value_parameters.warning ~current:true
"buffer contains addresses %a@." V.pretty v';
emit_alarm();
raise Abort_to_top
in
begin
if (Ival.is_zero iv) then (
Value_parameters.debug "Is_zero: rmax init";
racc :=
Ival.join !racc
(Ival.inject_singleton !offset) ;
continue := false;
) else if not(Ival.contains_zero iv) then (
Value_parameters.debug "No_zero: rmin init";
) else (
Value_parameters.debug "Neither: rmin init";
racc :=
Ival.join !racc
(Ival.inject_singleton !offset)
)
end
)
end;
if !continue then (
rival := Ival.add_int singleton_eight !rival;
offset := Int.succ !offset
)
done;
let racc = !racc in
let racc =
if Int.ge !offset max
then Ival.join racc (Ival.inject_singleton max)
else racc
in
let nacc = Ival.join acc_val racc in
Value_parameters.debug "nacc = %a" Ival.pretty nacc ;
nacc
) ival Ival.bottom
in
Value_parameters.debug "val_strlen = %a"
Ival.pretty val_strlen ;
val_strlen
in
let accumulate_one_offsetmap base ival acc =
Ival.join acc (do_one_offsetmap base ival)
in
let computed_strlen =
Cvalue.V.M.fold accumulate_one_offsetmap m Ival.bottom
in
Value_parameters.debug" size is %a" Ival.pretty computed_strlen ;
computed_strlen
with
| Abort_to_top
| Ival.Error_Top (* from fold_enum *) -> Ival.top
in
value
let frama_c_strlen state actuals =
if Value_parameters.ValShowProgress.get () then
Value_parameters.feedback ~current:true "Call to builtin strlen(%a)%t"
pretty_actuals actuals Value_util.pp_callstack;
match actuals with
| [ exp_str, str, _ ] ->
let notyet = ref true in
let emit_alarm () =
if !notyet
then begin
notyet := true;
Valarms.set_syntactic_context (Valarms.SyUnOp exp_str) ;
Valarms.warn_valid_string (warn_all_quiet_mode ())
end
in
let value =
abstract_strlen ~max:two61 ~emit_alarm str state
in
if Ival.is_bottom value
then
{ Value_types.c_values = [ None, Cvalue.Model.bottom];
c_clobbered = Base.SetLattice.bottom;
c_cacheable = Value_types.Cacheable;
}
else
{ Value_types.c_values =
[ Eval_op.wrap_size_t (V.inject_ival value), state ];
c_clobbered = Base.SetLattice.bottom;
c_cacheable = Value_types.Cacheable;
}
| _ ->
raise Db.Value.Aborted
let () = register_builtin "Frama_C_strlen" frama_c_strlen
let frama_c_strnlen state actuals =
if Value_parameters.ValShowProgress.get () then
Value_parameters.feedback ~current:true "Call to builtin strnlen(%a)%t"
pretty_actuals actuals Value_util.pp_callstack;
let notyet = ref true in
let emit_alarm () =
if !notyet
then begin
notyet := false;
Value_parameters.warning ~once:true ~current:true "assert (string valid up to n)";
end
in
try
( match actuals with
| [ (_exp_str, str, _); (_, n, _) ] ->
let n = V.project_ival n in
let max = Extlib.the (Ival.max_int n) in
let value = abstract_strlen ~max ~emit_alarm str state in
if Ival.is_bottom value
then
{ Value_types.c_values = [ None, Cvalue.Model.bottom];
c_clobbered = Base.SetLattice.bottom;
c_cacheable = Value_types.Cacheable;
}
else
let rangevalue =
Ival.inject_range (Some Int.zero) (Ival.max_int value)
in
let value = Ival.join value (Ival.narrow rangevalue n) in
{ Value_types.c_values =
[ Eval_op.wrap_size_t (V.inject_ival value), state ];
c_clobbered = Base.SetLattice.bottom;
c_cacheable = Value_types.Cacheable;
}
| _ ->
raise Db.Value.Aborted)
with
V.Not_based_on_null (* from project_ival *) ->
Value_parameters.warning ~once:true ~current:true
"assert(no address in second argument of strnlen)";
emit_alarm();
{ Value_types.c_values = [Eval_op.wrap_size_t V.top_int, state];
c_clobbered = Base.SetLattice.bottom;
c_cacheable = Value_types.Cacheable;
}
let () = register_builtin "Frama_C_strnlen" frama_c_strnlen
(* str(n)cmp builtins *)
let abstract_strcmp ~size ~signed ~min ~max ~emit_alarm
str1 syn1 str2 syn2 state =
(* Checks whether the call to strcmp respects the preconditions:
Calls emit_alarm syn? (e.g. to emit \valid_string(...))
if anything at all is wrong.
Returns top_int in most complicated cases
(e.g. too many offsets to consider)
*)
let make_with_alarms r =
let emit = { CilE.a_log = false; CilE.a_call = r } in
{ CilE.imprecision_tracing = CilE.a_ignore;
defined_logic = emit;
unspecified = emit;
others = emit;
}
in
( match str1, str2 with
| Location_Bytes.Top _, _ | _, Location_Bytes.Top _ ->
emit_alarm syn1;
emit_alarm syn2;
Ival.join Ival.minus_one Ival.zero_or_one
| Location_Bytes.Map _, Location_Bytes.Map _ ->
let negative_res = ref false in
let positive_res = ref false in
let zero_res = ref false in
let min = ref min in
let max = ref max in
let warn1 = ref false in
let warn2 = ref false in
let set_warn1 () = warn1 := true in
let set_warn2 () = warn2 := true in
let with_alarms1 = make_with_alarms set_warn1 in
let with_alarms2 = make_with_alarms set_warn2 in
let locb1 = ref (Locations.loc_bytes_to_loc_bits str1) in
let locb2 = ref (Locations.loc_bytes_to_loc_bits str2) in
let size_size = Int_Base.inject size in
let size_ival = Ival.inject_singleton size in
while Int.gt !max Int.zero do
let read_char_and_filter_0 warn with_alarms lobc
(chars_acc, locb_acc as acc) =
let loc = Locations.make_loc lobc size_size in
let char = Eval_op.find ~with_alarms state loc in
let char, address =
Cvalue.V.split Base.null char
in
if not (Cvalue.V.is_bottom address) then warn := true;
if Ival.is_bottom char
then acc
else begin
let char = Ival.cast ~size ~signed ~value:char in
Ival.join char chars_acc,
if Ival.is_zero char
then locb_acc
else
Location_Bits.join loc.Locations.loc locb_acc
end
in
let acc = Ival.bottom, Location_Bits.bottom in
let chars1, new_locb1 =
Location_Bits.fold_enum
(read_char_and_filter_0 warn1 with_alarms1)
!locb1
acc
in
let chars2, new_locb2 =
Location_Bits.fold_enum
(read_char_and_filter_0 warn2 with_alarms2)
!locb2
acc
in
(* Format.printf "iteration %a %a %a %a %B %B@."
Ival.pretty chars1 Ival.pretty chars2
Location_Bits.pretty new_locb1
Location_Bits.pretty new_locb2
!warn1 !warn2; *)
if Ival.is_bottom chars1
then begin
(* alarm already scheduled for str1, but what about str2? *)
if not !warn2
then ignore(abstract_strlen ~max:!max ~emit_alarm:set_warn2
str2 state);
max := Int.minus_one (* exit loop immediately *)
end
else if Ival.is_bottom chars2
then begin
if not !warn1
then ignore(abstract_strlen ~max:!max ~emit_alarm:set_warn1
str1 state);
max := Int.minus_one (* exit loop immediately *)
end
else
let f min1 max1 min2 max2 =
if Ival.compare_min_max min1 max2 < 0 then negative_res := true;
if Ival.compare_min_max min2 max1 < 0 then positive_res := true;
in
Ival.compare_C f chars1 chars2;
(* Format.printf "iteration--- pos:%B zero:%B neg:%B@."
!positive_res !zero_res !negative_res; *)
if not (Ival.intersects chars1 chars2)
then begin
(* check for well-formedness of the strings now since we
aren't going to finish reading them *)
(let max = !max in
if not !warn1
then ignore(abstract_strlen ~max ~emit_alarm:set_warn1 str1 state);
if not !warn2
then ignore(abstract_strlen ~max ~emit_alarm:set_warn2 str2 state));
max := Int.minus_one (* exit loop immediately *)
end
else begin
if Ival.contains_zero chars1 && Ival.contains_zero chars2
then zero_res := true;
if Location_Bits.is_bottom new_locb1
then begin
if not !warn2
then ignore(abstract_strlen ~max:!max ~emit_alarm:set_warn2
str2 state);
max := Int.minus_one (* exit loop immediately *)
end
else if Location_Bits.is_bottom new_locb2
then begin
if not !warn1
then ignore(abstract_strlen ~max:!max ~emit_alarm:set_warn1
str1 state);
max := Int.minus_one (* exit loop immediately *)
end
else begin
(* continue the loop; prepare next iteration *)
locb1 := Location_Bits.shift size_ival new_locb1;
locb2 := Location_Bits.shift size_ival new_locb2;
max := Int.pred !max;
min := Int.pred !min;
end
end;
done;
if !warn1 then emit_alarm syn1;
if !warn2 then emit_alarm syn2;
let res =
if !zero_res || Int.le !min Int.zero
then Ival.zero
else Ival.bottom
in
let res = if !positive_res then Ival.join Ival.one res else res in
if !negative_res then Ival.join Ival.minus_one res else res)
let frama_c_strcmp name ~size ~signed state actuals =
if Value_parameters.ValShowProgress.get () then
Value_parameters.feedback ~current:true "Call to builtin %s(%a)%t"
name
pretty_actuals actuals Value_util.pp_callstack;
match actuals with
| [ exp1, str1, _; exp2, str2, _ ] ->
let emit_alarm str =
Valarms.set_syntactic_context (Valarms.SyUnOp str) ;
Valarms.warn_valid_string (warn_all_quiet_mode ())
in
let value =
abstract_strcmp ~min:two61 ~max:two61 ~size ~signed
~emit_alarm str1 exp1 str2 exp2 state
in
if Ival.is_bottom value
then
{ Value_types.c_values = [ None, Cvalue.Model.bottom];
c_clobbered = Base.SetLattice.bottom;
c_cacheable = Value_types.Cacheable;
}
else
{ Value_types.c_values = [Eval_op.wrap_int (V.inject_ival value), state ];
c_clobbered = Base.SetLattice.bottom;
c_cacheable = Value_types.Cacheable;
}
| _ ->
raise Db.Value.Aborted
let frama_c_wcscmp state actuals =
let wchar = Cil.theMachine.Cil.wcharType in
let signed = Cil.isSignedInteger wchar in
let size = Int.of_int (Cil.bitsSizeOf wchar) in
Value_parameters.warning ~once:true "wcscmp builtin untested and known to emit the wrong alarm";
frama_c_strcmp "wcscmp" ~signed ~size state actuals
let frama_c_strcmp =
frama_c_strcmp "strcmp"
~signed:false (* C11 7.24.4:1 *) ~size:(Bit_utils.sizeofchar ())
let () = register_builtin "Frama_C_wcscmp" frama_c_wcscmp
let () = register_builtin "Frama_C_strcmp" frama_c_strcmp
let frama_c_strncmp name ~size ~signed state actuals =
if Value_parameters.ValShowProgress.get () then
Value_parameters.feedback ~current:true "Call to builtin %s(%a)%t"
name pretty_actuals actuals Value_util.pp_callstack;
match actuals with
| [ exp1, str1, _; exp2, str2, _; _, n, _ ] ->
let notyet = ref true in
let emit_alarm e =
if !notyet
then begin
notyet := false;
Value_parameters.warning ~once:true ~current:true
"assert (string %a valid up to n)" Printer.pp_exp e;
end
in
let n = V.project_ival n in
let min = Extlib.the (Ival.min_int n) in
let max = Extlib.the (Ival.max_int n) in
let value =
abstract_strcmp ~min ~max ~emit_alarm ~signed ~size
str1 exp1 str2 exp2 state
in
if Ival.is_bottom value
then
{ Value_types.c_values = [ None, Cvalue.Model.bottom];
c_clobbered = Base.SetLattice.bottom;
c_cacheable = Value_types.Cacheable;
}
else
{ Value_types.c_values = [Eval_op.wrap_int (V.inject_ival value), state ];
c_clobbered = Base.SetLattice.bottom;
c_cacheable = Value_types.Cacheable;
}
| _ ->
raise Db.Value.Aborted
let frama_c_wcsncmp state actuals =
let wchar = Cil.theMachine.Cil.wcharType in
let signed = Cil.isSignedInteger wchar in
let size = Int.of_int (Cil.bitsSizeOf wchar) in
Value_parameters.warning ~once:true "wcsncmp builtin untested and known to emit the wrong alarm";
frama_c_strncmp "wcsncmp" ~signed ~size state actuals
let frama_c_strncmp =
frama_c_strncmp "strncmp"
~signed:false (* C11 7.24.4:1 *) ~size:(Bit_utils.sizeofchar ())
let () = register_builtin "Frama_C_wcsncmp" frama_c_wcsncmp
let () = register_builtin "Frama_C_strncmp" frama_c_strncmp
(* memcmp builtin *)
let int_hrange = Int.two_power_of_int (8 * Cil.theMachine.Cil.theMachine.sizeof_int -1)
let int_neg_ival () =
Ival.inject_range
(Some (Int.neg int_hrange))
(Some (Int.of_int (-1)))
let int_pos_ival () =
Ival.inject_range
(Some Int.one)
(Some (Int.pred int_hrange))
let int_nonpos_ival () =
Ival.inject_range
(Some (Int.neg int_hrange))
(Some Int.zero)
let int_nonneg_ival () =
Ival.inject_range
(Some Int.zero)
(Some (Int.pred int_hrange))
let memcmp_ivals lival1 lival2 validity1 validity2 offsetmap1 offsetmap2 size =
Ival.fold_enum
(fun ival1 acc_val1 ->
if (Cvalue.V.is_topint acc_val1) then raise Abort_to_top ;
let rival1 = ref (Ival.mul ival1 (Ival.inject_singleton Int.eight)) in
let val_cmp2 =
Ival.fold_enum
(fun ival2 acc_val2 ->
if (Cvalue.V.is_topint acc_val2) then raise Abort_to_top ;
let rival2 = ref (Ival.scale Int.eight ival2) in
let offset = ref 0
and continue = ref true
and racc = ref acc_val2 in
while(!continue && (!offset < size) && not (Cvalue.V.is_topint !racc)) do
(*
Value_parameters.feedback "reading at rival1=%a rival2=%a"
Ival.pretty !rival1 Ival.pretty !rival2 ;
*)
let find ~validity ~offsets offm =
match offm with
| `Bottom -> true, V_Or_Uninitialized.bottom
| `Top -> raise Abort_to_top
| `Map m ->
Cvalue.V_Offsetmap.find ~validity ~offsets ~size:Int.eight m
in
let _, v1 = find ~validity:validity1 ~offsets:!rival1 offsetmap1
and _, v2 = find ~validity:validity2 ~offsets:!rival2 offsetmap2
in
if not (is_init v1 && is_init v2) then
begin
(* should be a runtime error: read uninitialized value *)
Value_parameters.feedback
"Frama_C_memcmp: potential rte (read uninit)" ;
racc := Cvalue.V.top_int ;
continue := false
end
else
let w1 = Cvalue.V_Or_Uninitialized.get_v v1
and w2 = Cvalue.V_Or_Uninitialized.get_v v2 in
if (Cvalue.V.is_bottom w1) || (Cvalue.V.is_bottom w2) then (
(* should be a runtime error: read out of bounds *)
Value_parameters.feedback
"Frama_C_rte: potential rte (read out of bounds)";
racc := Cvalue.V.top_int ;
continue := false
) else (
let iv1 =
Ival.cast ~size:Int.eight ~signed:false
~value:(Cvalue.V.project_ival w1)
and iv2 =
Ival.cast ~size:Int.eight ~signed:false
~value:(Cvalue.V.project_ival w2) in
if (Ival.is_singleton_int iv1) && (Ival.is_singleton_int iv2) then (
match Ival.min_int iv1, Ival.min_int iv2 with
| Some u1, Some u2 ->
let cmp = Abstract_interp.Int.compare u1 u2 in
if (cmp < 0) then (
continue := false ;
racc :=
Cvalue.V.inject_ival (int_neg_ival ())
) else if (cmp > 0) then (
continue := false ;
racc :=
Cvalue.V.inject_ival (int_pos_ival ())
) (* else continue *)
| _, _ -> assert false
) else
let lower1,upper1 = Ival.min_and_max iv1
and lower2,upper2 = Ival.min_and_max iv2 in
match upper1,lower2 with
| Some u, Some l ->
let cmp = Abstract_interp.Int.compare u l in
if cmp < 0 then (
continue := false ;
racc :=
Cvalue.V.inject_ival (int_neg_ival ())
) else if (cmp = 0) then (
racc :=
Cvalue.V.inject_ival (int_nonpos_ival ())
(* and continue *)
) else (
match upper2, lower1 with
| Some u, Some l ->
let cmp = Abstract_interp.Int.compare u l in
if (cmp < 0) then (
continue := false;
racc :=
Cvalue.V.inject_ival (int_pos_ival ())
) else if (cmp = 0) then (
racc :=
Cvalue.V.inject_ival (int_nonneg_ival ())
(* and continue *)
) else racc := Cvalue.V.top_int (* continue := false *)
| _, _ -> assert false
)
| _, _ -> assert false
)
;
if !continue then (
rival1 :=
Ival.add_int
(Ival.inject_singleton Int.eight)
!rival1
;
rival2 :=
Ival.add_int
(Ival.inject_singleton Int.eight)
!rival2
;
incr offset
)
done
;
if Cvalue.V.is_bottom !racc then
racc := Cvalue.V.inject_ival (Ival.zero)
;
Cvalue.V.join acc_val2 !racc
) lival2 Cvalue.V.bottom
in
Cvalue.V.join acc_val1 val_cmp2
) lival1 Cvalue.V.bottom
let frama_c_memcmp state actuals =
let compute (exp_fst,fst,_) (_exp_snd,snd,_) (exp_size,size,_) =
if Value_parameters.ValShowProgress.get () then
Value_parameters.feedback ~current:true "Call to builtin memcmp(%a)%t"
pretty_actuals actuals Value_util.pp_callstack;
if V.equal size V.singleton_zero
then
{ Value_types.c_values = [Eval_op.wrap_int V.singleton_zero, state];
c_clobbered = Base.SetLattice.bottom;
c_cacheable = Value_types.Cacheable;
}
else
try
let plevel = Value_parameters.ArrayPrecisionLevel.get() in
let _with_alarms = warn_all_quiet_mode () in
let size =
try
V.project_ival size
with V.Not_based_on_null ->
Value_parameters.feedback ~current:true
"Call to builtin memcmp(): address as size";
raise Abort_to_top
in
let _min,max = Ival.min_and_max size in
let max = match max with None -> assert false (* TODO *) | Some m -> m in
let term_size = Logic_utils.expr_to_term ~cast:true exp_size in
let array_fst = Logic_utils.array_with_range exp_fst term_size in
Valarms.set_syntactic_context (Valarms.SyMemLogic array_fst);
let val_cmp = (
match fst, snd with
| Cvalue.V.Top(_,_), _
| _, Cvalue.V.Top(_,_) -> Cvalue.V.top_int
| Cvalue.V.Map m1, Cvalue.V.Map m2 ->
Cvalue.V.M.fold
(fun base1 ival1 acc1 ->
if Cvalue.V.is_topint acc1 then raise Abort_to_top ;
let validity1 = Base.validity base1 in
let offsetmap1 =
Cvalue.Model.find_base_or_default base1 state
in
let val_cmp0 =
Cvalue.V.M.fold
(fun base2 ival2 acc2 ->
if (Cvalue.V.is_topint acc2) then raise Abort_to_top ;
let validity2 = Base.validity base2 in
let offsetmap2 =
Cvalue.Model.find_base_or_default base2 state
in
let val_cmp1 =
if Int.compare max (Int.of_int plevel) > 0 then
raise Abort_to_top
else
memcmp_ivals ival1 ival2
validity1 validity2
offsetmap1 offsetmap2
(Int.to_int max)
in Cvalue.V.join acc2 val_cmp1
) m2 Cvalue.V.bottom
in Cvalue.V.join acc1 val_cmp0
) m1 Cvalue.V.bottom
)
in
{ Value_types.c_values = [Eval_op.wrap_int val_cmp, state];
c_clobbered = Base.SetLattice.bottom;
c_cacheable = Value_types.Cacheable;
}
with
Abort_to_top
| Ival.Error_Top (* from fold_enum *) ->
{ Value_types.c_values = [Eval_op.wrap_int V.top_int, state];
c_clobbered = Base.SetLattice.bottom;
c_cacheable = Value_types.Cacheable;
}
in
try
match actuals with
| [fst; snd; size] ->
compute fst snd size
| _ -> raise Db.Value.Outside_builtin_possibilities
with
| Db.Value.Outside_builtin_possibilities ->
Value_parameters.result
"Invalid call to Frama_C_memcmp builtin %a%t"
pretty_actuals actuals Value_util.pp_callstack;
raise Db.Value.Outside_builtin_possibilities
| Db.Value.Aborted ->
Value_parameters.error
"Invalid call to Frama_C_memcmp%a" pretty_actuals actuals;
raise Db.Value.Aborted
let () = register_builtin "Frama_C_memcmp" frama_c_memcmp
let frama_c_interval_split state actuals =
try
begin match actuals with
......
src/plugins/value/builtins_nonfree_string.ml 0 → 100644
+ 1553
− 0
View file @ 41235626
This diff is collapsed.
src/plugins/value/builtins_nonfree_string.mli 0 → 100644
+ 17
− 0
View file @ 41235626
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* *)
(* Copyright (C) 2007-2015 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
(* All rights reserved. *)
(* Contact CEA LIST for licensing. *)
(* *)
(**************************************************************************)
(** Non-free Value builtins. Contact CEA LIST for licensing *)
(** Nothing is exported, all the builtins are registered through
{Builtins.register_builtin} *)
tests/non-free/cmp.c deleted 100644 → 0
+ 0
− 9
View file @ d825c057
/* run.config
OPT: -cpp-extra-args="-nostdinc -Ishare/libc" -val -no-results -val-builtin memcmp:Frama_C_memcmp
*/
#include "string.h"
int main(int c, int d){
memcmp(c, d, 0);
}
tests/non-free/memchr.c 0 → 100644
+ 575
− 0
View file @ 41235626
#include "__fc_builtin.h"
static volatile int nondet;
#define assert_bottom(exp,id) if (nondet) { exp; Frama_C_show_each_unreachable_ ## id(); }
#define memchr Frama_C_memchr
//@ assigns \result \from ((char*)s)[0..], c, n;
void *Frama_C_memchr(const void *s, int c, size_t n);
const char* static_str = "Hello World\n";
const char* zero_str = "abc\0\0\0abc";
#define TSZ 12
// Definitions for C++ oracle checking
typedef int Ival;
typedef int RES;
#define NONDET(a,b) (nondet ? (a) : (b))
#define IF_NONDET(var,val) if (nondet) var = val
#define RANGE(from,to) Frama_C_interval(from,to)
#define CHAR_ARRAY(var,n) char var[n]
#define CHAR_PTR(var) char *var
#define STRING(var,str) var = str;
const char* tab_str[TSZ] =
{
"" , // 0
"a", // 1
"aa" , // 2
"aaa" , // 3
"aaaa" , // 4
"aaaaa" , // 5
"aaaaaa" , // 6
/* hole */
"aaaaaaaaa" , // 9
"aaaaaaaaaa" ,
"aaaaaaaaaaa",
"aaaaaaaaaaaa" ,
"aaaaaaaaaaaaa" }; // 13
char unterminated_string[12] = "unterminated";
int my_memchr(const void *p, size_t offs, int c, size_t n) {
const char *s = (const char*) p;
char *ss = memchr(s+offs,c,n);
int res;
if (ss == 0) {
res = -1;
} else {
res = ss - p;
}
Frama_C_show_each_mymemchr(res);
return res;
}
int my_memchr2(const void *p, const void *base, size_t offs, int c, size_t n) {
char *s = memchr(((const char *)p)+offs,c,n);
int res;
if (s == 0) {
res = -1;
} else {
res = s - base;
}
Frama_C_show_each_mymemchr2(res);
return res;
}
void small_sets(char c) {
CHAR_PTR(s);
STRING(s,"abc");
Ival o = NONDET(0, 1);
RES z1 = my_memchr(s, o, c, 4);
//@ assert (z1 == 2 || z1 == 3);
STRING(s,"\0bc");
o = NONDET(0,1);
RES z2 = my_memchr(s, o, c, 3);
Frama_C_show_each_z2(z2);
//@ assert (z2 == 0 || z2 == 2);
STRING(s,"");
RES z3 = my_memchr(s, 0, c, 0);
//@ assert (z3 == -1);
STRING(s,"b\0c");
o = NONDET(0,2);
RES z4 = my_memchr(s, o, c, 2);
//@ assert (z4 == 1);
CHAR_ARRAY(t, 4);
t[0] = t[1] = NONDET(0, 1);
t[2] = t[3] = 1;
RES z5 = my_memchr(t, 0, c, 4); // no warning
//@ assert z5 == -1 || z5 == 0 || z5 == 1;
}
void zero_termination(char c) {
CHAR_ARRAY(empty_or_non_terminated, 1);
empty_or_non_terminated[0] = NONDET(0, 100);
RES z1 = my_memchr(empty_or_non_terminated, 0, c, 1);
//@ assert z1 == -1 || z1 == 0;
CHAR_ARRAY(non_terminated, 1);
non_terminated[0] = 'X';
RES z2 = my_memchr(non_terminated, 0, c, 1);
//@ assert z2 == -1;
assert_bottom(my_memchr(non_terminated, 0, c, 2), non_terminated);
CHAR_ARRAY(non_terminated2, 4);
non_terminated2[0] = 76; non_terminated2[1] = 0;
non_terminated2[2] = 28; non_terminated2[3] = 14;
Ival o = NONDET(2, 3);
assert_bottom(my_memchr(non_terminated2, o, c, 4), non_terminated2);
}
void initialization(char c) {
char empty_or_uninitialized[1];
IF_NONDET(empty_or_uninitialized[0], 0);
RES z1 = my_memchr(empty_or_uninitialized, 0, c, 1);
//@ assert (z1 == -1 || z1 == 0);
char uninitialized[1];
assert_bottom(my_memchr(uninitialized, 0, c, 1),uninitialized);
CHAR_ARRAY(s, 2);
IF_NONDET(s[0], 1);
s[1] = 0;
RES z2 = my_memchr(s, 0, c, 2);
//@ assert (z2 == 1);
CHAR_ARRAY(t,4);
t[0] = t[1] = 10;
IF_NONDET(t[2], 10);
t[3] = 0;
RES z3 = my_memchr(t, 0, c, 4);
//@ assert (z3 == 3);
}
typedef struct {
int a:8;
int b:8;
int c:17;
} st;
void bitfields(char c) {
st s;
s.a = 3;
s.b = 1;
s.c = 7;
char *p = &s;
assert_bottom(Frama_C_memchr(p, c, 3),bitfields);
}
typedef struct {
int a:4;
int b:4;
int c:17;
} st2;
void bitfields2(char c) {
st2 s;
s.a = 3;
s.b = 1;
s.c = 7;
char *p = &s;
RES z1 = my_memchr(p, 0, c, 3);
//@assert (z1 == 2);
}
void init_array_nondet(char *a, int from, int to, int val1, int val2) {
int val = nondet ? val1 : val2;
Frama_C_memset(a + from, val, to-from+1);
from = to = val1 = val2 = -1; // reset to minimize oracle changes
}
void large(char c) {
char a[100];
init_array_nondet(a, 0, 99, 1, 2);
a[20] = 0;
a[75] = 0;
Ival offset = RANGE(3, 30);
RES z1 = my_memchr(a, offset, c, 100);
//@ assert (z1 >= 0 && z1 <= 54);
offset = RANGE(5, 17);
RES z2 = my_memchr(a, offset, c, 100);
//@ assert (z2 >= 3 && z2 <= 15);
offset = RANGE(60, 74);
RES z3 = my_memchr(a, offset, c, 100);
//@ assert (z3 >= 1 && z3 <= 15);
offset = RANGE(63, 80);
RES z4 = my_memchr(a, offset, c, 100);
//@ assert (z4 >= 0 && z4 <= 12);
init_array_nondet(a, 0, 99, 0, 2);
offset = RANGE(50, 70);
RES z5 = my_memchr(a, offset, c, 100);
//@ assert (z5 >= 0 && z5 <= 49);
}
void large_uninit(char c) {
char a[100];
init_array_nondet(a, 0, 39, 1, 2);
init_array_nondet(a, 50, 94, 3, 4);
a[20] = 0;
a[75] = 0;
Ival offset = RANGE(3, 30);
RES z1 = my_memchr(a, offset, c, 100);
//@ assert (z1 >= 0 && z1 <= 17);
a[98] = 0;
offset = RANGE(63, 80);
RES z2 = my_memchr(a, offset, c, 100);
//@ assert (z2 >= 0 && z2 <= 12);
offset = RANGE(45, 55);
RES z3 = my_memchr(a, offset, c, 100);
//@ assert (z3 >= 20 && z3 <= 25);
offset = 0; // avoid oracle diffs when changed
}
void escaping(char c) {
CHAR_ARRAY(s,4);
{
int x;
*((int *)s) = &x;
}
IF_NONDET(s[0], 0);
RES z1 = my_memchr(s, 0, c, 4); // alarm
//@ assert (z1 == 0);
s[0] = 0;
RES z2 = my_memchr(s, 0, c, 4); // no alarm
//@ assert (z2 == 0);
}
void misc(char c) {
const char* loc_str = "Bonjour Monde\n";
char loc_char_array[5];
RES sz1,sz2,sz3,sz4,sz5,sz6,sz7,sz8;
int x = 0xabcdef00;
RES z = 0x12345600;
int i;
char *str;
assert_bottom(Frama_C_memchr(unterminated_string, c, 13),unterminated_string);
str = nondet ? static_str : loc_str;
sz1 = my_memchr(str, 0, c, 15);
//@ assert(sz1 == 12 || sz1 == 14);
str = &x;
char *base = str;
str = nondet ? str : str + 3;
sz2 = my_memchr2(str, base, 0, c, 12);
//@ assert(sz2 == 0) ; // no, could also do an RTE
i = Frama_C_interval(0,TSZ-1);
str = tab_str[i];
sz3 = my_memchr(str, 0, c, 14);
//@ assert(sz3 >= 0 && sz3 <= 13);
loc_char_array[3] = '\0';
assert_bottom(my_memchr(loc_char_array, 0, c, 5),loc_char_array);
sz4 = my_memchr(zero_str, 0, c, 9);
//@ assert(sz4 == 3);
char *s1 = nondet ? "abc" : "ABCD";
char *s2 = nondet ? s1 : s1+1;
sz5 = my_memchr2(s2, s1, 0, c, 5);
//@ assert(sz5 >= 2 && sz5 <= 4);
s1 = nondet ? "efg" : "EFGH";
s2 = nondet ? s1+1 : s1+2;
sz6 = my_memchr2(s2, s1, 0, c, 5);
//@ assert(sz6 >= 1 && sz6 <= 3);
s1 = nondet ? "mno\0pqr" : "MNOP\0QRS";
for (int j = 0; j < 8; j++) {
sz7 = my_memchr(s1, j, c, 10);
//@ assert(sz7 >= 0 && sz7 <= 4);
}
char maybe_init[2];
maybe_init[1] = '\0';
IF_NONDET(maybe_init[0], 'A');
sz8 = my_memchr(maybe_init, 0, c, 2);
//@ assert(sz8 == 1);
}
void big_array (char c) {
int u[200];
int r[201];
int t[1000000];
int *p;
p = &u[nondet];
*p = 0x10230067;
p = &r[nondet];
*p = 0x10230067;
p = &t[nondet];
*p = 0x10230067;
unsigned long len_u;
unsigned long len_r;
unsigned long len_t;
len_u = my_memchr(u, 0, c, 800); // below plevel; precise
len_r = my_memchr(r, 0, c, 805); // above plevel; imprecise
len_t = my_memchr(t, 0, c, 4000001); // *far* above plevel
Frama_C_show_each(len_u, len_r, len_t);
//@ assert len_u == 1;
//@ assert len_r >= 1 && len_r <= 801;
//@ assert len_t >= 1 && len_t <= 3999997;
len_u = my_memchr(u, 0, c, 1600); // should be precise
len_r = my_memchr(r, 0, c, 1608);
len_t = my_memchr(t, 0, c, 8000000);
Frama_C_show_each(len_u, len_r, len_t);
//@ assert len_u >= 0 && len_u <= 3;
//@ assert len_r >= 0 && len_r <= 802;
//@ assert len_t >= 0 && len_t <= 3999998;
}
void no_zero_but_ok(char c) {
CHAR_ARRAY(s,20);
s[0] = s[1] = s[2] = s[3] = s[4] = s[5] = s[6] = s[7] = s[8] = s[9] = 1;
s[10] = 0;
s[11] = s[12] = s[13] = 1;
s[14] = s[15] = s[16] = s[17] = s[18] = s[19] = nondet ? 1 : 0;
RES z1 = my_memchr(s, 0, c, 5);
//@assert z1 == -1;
RES z2 = my_memchr(s, 0, c, 11);
//@assert z2 == 10;
char *p = nondet ? s+1 : s+8;
RES z3 = my_memchr2(p, s, 0, c, 11);
//@assert z3 == 2 || z3 == 9;
p = nondet ? s+7 : s+11;
RES z4 = my_memchr2(p, s, 0, c, 4);
//@assert z4 == -1 || z4 == 3;
p = nondet ? s+7 : s+18;
RES z5 = my_memchr2(p, s, 0, c, 5); // maybe_indet = true
//@assert z5 == 0 || z5 == 1 || z5 == 3;
}
void small_sets_n(char c) {
char *s;
STRING(s,"abcde");
char *p = nondet ? s : s+1;
char n = nondet ? 2 : 5;
RES z1 = my_memchr2(p, s, 0, c, n);
//@assert z1 == -1 || z1 == 4;
STRING(s,"\0bcdef");
p = nondet ? s : s+1;
n = nondet ? 1 : 6;
RES z2 = my_memchr2(p, s, 0, c, n);
//@assert z2 == -1 || z2 == 0 || z2 == 5;
STRING(s,"bcd\0efg");
p = nondet ? s : s+2;
RES z3a = my_memchr2(p, s, 0, c, 4);
//@assert z3a == 1 || z3a == 3;
p = nondet ? s : s+2;
n = nondet ? 3 : 4;
RES z3b = my_memchr2(p, s, 0, c, n);
//@assert z3b == -1 || z3b == 1 || z3b == 3;
p = nondet ? s : s+2;
n = nondet ? 2 : 3;
RES z3 = my_memchr2(p, s, 0, c, n);
//@assert z3 == -1 || z3 == 1;
p = nondet ? s : nondet ? s+2 : s+4;
n = nondet ? 2 : 7;
RES z4 = my_memchr2(p, s, 0, c, n); // alarm
//@assert z4 == -1 || z4 == 1 || z4 == 3;
}
void large_n(char c) {
CHAR_ARRAY(a, 100);
init_array_nondet(a, 0, 99, 1, 2);
a[15] = 0;
a[28] = 0;
a[40] = 0;
a[75] = 0;
Ival offset = RANGE(3, 30);
Ival n = RANGE(10, 20);
RES z1 = my_memchr(a, offset, c, n);
//@assert -1 <= z1 <= 12;
a[28] = 1;
a[29] = 0;
RES z2 = my_memchr(a, offset, c, n);
//@assert -1 <= z2 <= 13;
a[40] = 1;
RES z3 = my_memchr(a, offset, c, n); // no alarm
//@assert -1 <= z3 <= 13;
offset = RANGE(5, 17);
RES z4 = my_memchr(a, offset, c, n);
//@assert -1 <= z4 <= 13;
offset = RANGE(60, 74);
RES z5 = my_memchr(a, offset, c, n);
//@assert -1 <= z5 <= 15;
offset = RANGE(63, 80);
RES z6 = my_memchr(a, offset, c, n); // no alarm
//@assert -1 <= z6 <= 12;
init_array_nondet(a, 0, 99, 0, 2);
offset = RANGE(50, 70);
RES z7 = my_memchr(a, offset, c, n);
//@assert -1 <= z7 <= 19;
n = RANGE(0, 100);
RES z8 = my_memchr(a, offset, c, n); // alarm
//@assert -1 <= z8 <= 49;
offset = RANGE(0, 10);
n = RANGE(0, 90);
RES z9 = my_memchr(a, offset, c, n); // no alarm
//@assert -1 <= z9 <= 89;
}
void unbounded_n(char c) {
int n = nondet;
if (n < 0) n = 0;
char *s;
STRING(s,"abc");
RES zu1 = my_memchr(s, 0, c, n);
//@ assert zu1 == -1 || zu1 == 3;
Ival o = NONDET(0,1);
RES zu2 = my_memchr(s, o, c, n);
//@ assert zu2 == -1 || zu2 == 2 || zu2 == 3;
STRING(s,"bcd\0eg");
RES zu3 = my_memchr(s, 0, c, n);
//@ assert zu3 == -1 || zu3 == 3;
}
void intervals(char c) {
CHAR_ARRAY(a, 100);
init_array_nondet(a, 0, 9, 0, 1);
init_array_nondet(a, 3, 6, 1, 1);
init_array_nondet(a, 11, 11, 0, 1);
init_array_nondet(a, 12, 15, 1, 1);
init_array_nondet(a, 16, 19, 0, 1);
Ival offset = RANGE(0,9);
Ival n = RANGE(0, 10);
RES z1 = my_memchr(a, offset, c, n);
//@ assert z1 >= -1 && z1 <= 9;
offset = RANGE(3,9);
n = RANGE(2,10);
RES z2 = my_memchr(a, offset, c, n);
//@ assert z2 >= -1 && z2 <= 6;
offset = RANGE(3,9);
n = RANGE(0,11);
RES z3 = my_memchr(a, offset, c, n);
//@ assert z3 >= -1 && z3 <= 6;
offset = RANGE(3,10);
n = RANGE(0,9);
RES z4 = my_memchr(a, offset, c, n);
//@ assert z4 >= -1 && z4 <= 6;
offset = RANGE(3,10);
n = RANGE(0,10);
RES z5 = my_memchr(a, offset, c, n);
//@ assert z5 >= -1 && z5 <= 6;
offset = RANGE(3,10);
n = RANGE(0,11);
RES z6 = my_memchr(a, offset, c, n);
//@ assert z6 >= -1 && z6 <= 6;
offset = RANGE(3,11);
n = RANGE(0,10);
RES z7 = my_memchr(a, offset, c, n);
//@ assert z7 >= -1 && z7 <= 8;
offset = RANGE(3,11);
n = RANGE(0,10);
RES z8 = my_memchr(a, offset, c, n);
//@ assert z8 >= -1 && z8 <= 8;
offset = RANGE(3,11);
n = RANGE(0,11);
RES z9 = my_memchr(a, offset, c, n);
//@ assert z9 >= -1 && z9 <= 8;
}
void small_sets_no_assertions(char c, RES *res) {
CHAR_PTR(s);
STRING(s,"abc");
Ival o = NONDET(0, 1);
res[0] = my_memchr(s, o, c, 4);
STRING(s,"\0bc");
o = NONDET(0,1);
res[1] = my_memchr(s, o, c, 3);
STRING(s,"");
res[2] = my_memchr(s, 0, c, 0);
STRING(s,"b\0c");
o = NONDET(0,2);
res[3] = my_memchr(s, o, c, 2);
CHAR_ARRAY(t, 4);
t[0] = t[1] = NONDET(c, 1);
t[2] = t[3] = 1;
res[4] = my_memchr(t, 0, c, 4);
}
void small_sets_chars() {
char c = 'a';
RES res[5];
small_sets_no_assertions(c, res);
Frama_C_show_each_res_a(res[0], res[1], res[2], res[3], res[4]);
//@ assert res[0] == 0 || res[0] == -1; // alarm
//@ assert res[1] == -1; // no alarm
//@ assert res[2] == -1; // no alarm
//@ assert res[3] == -1; // no alarm
//@ assert res[4] == -1 || res[4] == 0 || res[4] == 1; // no alarm
c = 'b';
small_sets_no_assertions(c, res);
Frama_C_show_each_res_b(res[0], res[1], res[2], res[3], res[4]);
//@ assert res[0] == 0 || res[0] == 1; // no alarm
//@ assert res[1] == 0 || res[1] == 1; // no alarm
//@ assert res[2] == -1; // no alarm
//@ assert res[3] == -1 || res[3] == 0; // no alarm
//@ assert res[4] == -1 || res[4] == 0 || res[4] == 1; // no alarm
c = nondet ? 'a' : 'b'; // c IN {a; b}
small_sets_no_assertions(c, res);
Frama_C_show_each_res_a_b(res[0], res[1], res[2], res[3], res[4]);
//@ assert res[0] == -1 || res[0] == 0 || res[0] == 1; // alarm
//@ assert res[1] == -1 || res[1] == 0 || res[1] == 1; // no alarm
//@ assert res[2] == -1; // no alarm
//@ assert res[3] == -1 || res[3] == 0; // no alarm
//@ assert res[4] == -1 || res[4] == 0 || res[4] == 1; // no alarm
c = nondet ? 'b' : 'c'; // c IN {b; c}
small_sets_no_assertions(c, res);
Frama_C_show_each_res_b_c(res[0], res[1], res[2], res[3], res[4]);
//@ assert -1 <= res[0] && res[0] <= 2; // no alarm
//@ assert -1 <= res[1] && res[1] <= 2; // no alarm
//@ assert res[2] == -1; // no alarm
//@ assert res[3] == -1 || res[3] == 0 || res[3] == 2; // no alarm
//@ assert res[4] == -1 || res[4] == 0 || res[4] == 1; // no alarm
if (nondet) c = 0; // c IN {b; c; 0}
small_sets_no_assertions(c, res);
Frama_C_show_each_res_b_c_0(res[0], res[1], res[2], res[3], res[4]);
//@ assert -1 <= res[0] && res[0] <= 3; // no alarm
//@ assert -1 <= res[1] && res[1] <= 2; // no alarm
//@ assert res[2] == -1 || res[2] == 0; // no alarm
//@ assert -1 <= res[3] && res[3] <= 2; // no alarm
//@ assert res[4] == -1 || res[4] == 0 || res[4] == 1; // no alarm
}
int main () {
char c = 0;
small_sets(c);
zero_termination(c);
initialization(c);
large(c);
large_uninit(c);
misc(c);
bitfields(c);
bitfields2(c);
escaping(c);
big_array(c);
no_zero_but_ok(c);
small_sets_n(c);
large_n(c);
unbounded_n(c);
intervals(c);
small_sets_chars();
return 0;
}
tests/non-free/memcmp.c deleted 100644 → 0
+ 0
− 46
View file @ d825c057
/* run.config
STDOPT:
*/
#include "__fc_builtin.h"
/*@ assigns \result \from ((char*)s1)[0.. n-1], ((char*)s2)[0.. n-1]; */
extern int Frama_C_memcmp (const void *s1, const void *s2, size_t n);
int main() {
unsigned char t[6] = { 0xef, 0xcd , 0xab , 0x00, 0x01, 0x01 };
char s[6] = { 0xef, 0xcd , 0xab , 0x00, 0x01, 0x01 };
const char* s1 = "hello world\n";
const char* s2 = "bla+hello world\n";
int x = 0x00abcdef;
int y = 0x01abcdef;
int z = Frama_C_memcmp(&x,&x,4);
//@ assert(z == 0);
int a = Frama_C_memcmp(&x,&y,4);
//@ assert(a < 0);
int b = Frama_C_memcmp(&y,&x,4);
//@ assert(b > 0);
int c = Frama_C_memcmp(&x,t,4);
//@ assert(c == 0);
int d = Frama_C_memcmp(t,&x,4);
//@ assert(d == 0);
int e = Frama_C_memcmp(s,&x,4);
//@ assert(e == 0);
int f = Frama_C_memcmp(&x,s,4);
//@ assert(f == 0);
// int g = Frama_C_memcmp(&x,s,6);
int h = Frama_C_memcmp(s1,s2+4,13);
//@ assert(h == 0);
return 0;
}
tests/non-free/oracle/memchr.err.oracle 0 → 100644
+ 0
− 0
View file @ 41235626
tests/non-free/oracle/memchr.res.oracle 0 → 100644
+ 1775
− 0
View file @ 41235626
This diff is collapsed.
tests/non-free/oracle/strchr.err.oracle 0 → 100644
+ 0
− 0
View file @ 41235626
tests/non-free/oracle/strchr.res.oracle 0 → 100644
+ 1497
− 0
View file @ 41235626
This diff is collapsed.
tests/non-free/oracle/strlen.res.oracle
+ 445
− 38
View file @ 41235626
This diff is collapsed.
tests/non-free/oracle/strnlen.res.oracle
+ 2
− 1
View file @ 41235626
......@@ -18,7 +18,8 @@
tests/non-free/strnlen.i:9:[value] Call to builtin strnlen(({{ &t1[0] }},{3}))
tests/non-free/strnlen.i:10:[value] Call to builtin strnlen(({{ &t1[0] }},{5}))
tests/non-free/strnlen.i:11:[value] Call to builtin strnlen(({{ &t1[0] }},{6}))
tests/non-free/strnlen.i:11:[value] warning: assert (string valid up to n)
tests/non-free/strnlen.i:11:[value] warning: built-in strnlen: tests/non-free/strnlen.i:11:
reading indeterminate data
tests/non-free/strnlen.i:13:[value] Call to builtin strnlen(({{ &t2[0] }},{3}))
tests/non-free/strnlen.i:14:[value] Call to builtin strnlen(({{ &t2[0] }},{5}))
tests/non-free/strnlen.i:15:[value] Call to builtin strnlen(({{ &t2[0] }},{6}))
......
tests/non-free/oracle/strnlen2.err.oracle 0 → 100644
+ 0
− 0
View file @ 41235626
tests/non-free/oracle/strnlen2.res.oracle 0 → 100644
+ 920
− 0
View file @ 41235626
This diff is collapsed.
tests/non-free/strchr.c 0 → 100644
+ 469
− 0
View file @ 41235626
This diff is collapsed.
tests/non-free/strcmp.c deleted 100644 → 0
+ 0
− 127
View file @ d825c057
/* run.config
OPT: -val -journal-disable -val-builtin printf:Frama_C_printf -val-builtin strcmp:Frama_C_strcmp -val-builtin strncmp:Frama_C_strncmp
*/
/*@ assigns \result \from s1[0..], s2[0..]; */
int strcmp(const char *s1, const char *s2);
/*@ assigns \result \from s1[0..], s2[0..], n; */
int strncmp(const char *s1, const char *s2, unsigned long n);
/*@ assigns \nothing; */
int printf(const char *fmt, ...);
char *toto0 = "toto";
char *abc0 = "abc";
char *abd0 = "abd";
char *a0 = "a";
char abc[3] = "abc";
char string_with_addr[] = "qwertyuioop";
char string[] = "qwertyuioop";
char commonv[] = "common variation";
char commonf[] = "common fugue";
volatile int u;
char tmp[2];
int t;
void expect(int a)
{
printf("expect %d: %d\n", a, t);
}
int main() {
int r1a, r2a, r3a, r4a;
t = strcmp(toto0, toto0);
expect(0);
t = strcmp(abd0, abc0);
expect(1);
t = strcmp(abc0, a0);
expect(1);
t = strcmp(a0, abc0);
expect(-1);
t = strcmp("bbc", abc0);
expect(1);
t = strcmp(abc0, "bbc");
expect(-1);
t = strcmp(abc0, abd0);
expect(-1);
t = strcmp(commonf, commonv);
expect(-1);
printf("strncmp:\n");
t = strncmp(abd0, abc0, 0);
expect(0);
t = strncmp(abd0, abc0, 1);
expect(0);
t = strncmp(abd0, abc0, 2);
expect(0);
t = strncmp(abd0, abc0, 3);
expect(1);
t = strncmp(abd0, abc0, 4);
expect(1);
t = strncmp(a0, abc0, 0);
expect(0);
t = strncmp(a0, abc0, 1);
expect(0);
t = strncmp(a0, "b", 0);
expect(0);
t = strncmp(a0, "b", 1);
expect(-1);
printf("char signedness tricks:\n");
t = strcmp(a0, "\300");
expect(-1);
tmp[0] = 192;
t = strcmp(a0, tmp);
expect(-1);
*(unsigned char *)tmp = 192;
t = strcmp(a0, tmp);
expect(-1);
printf("END OF DETERMINISTIC TESTS\n");
int rn1 = strncmp(abd0, abc0, 1 + !u);
int rn2 = strncmp(abd0, abc0, 2 + !u);
int rn3 = strncmp(abd0, abc0, 3 + !u);
char *p1 = u ? abd0 : "abb";
int r1_1m1 = strcmp(abc0, p1);
int r2_1m1 = strcmp(p1, abc0);
int r3_1m1, r4_m1;
if (u)
{
if (u) commonv[5] = 0;
r3_1m1 = strcmp(commonf, commonv);
}
else
{
if (u) commonf[5] = 0;
r4_m1 = strcmp(commonf, commonv);
}
int r5_10m1 = strcmp(commonf, commonv);
/* Alarms */
if (u)
r1a = strcmp(abc0, abc);
if (u)
r2a = strcmp(a0, abc);
*(void**)(string_with_addr+4) = &r1a;
if (u)
r3a = strcmp(string, string_with_addr);
if (u) *(void**)(string_with_addr+4) = 0;
if (u)
r4a = strcmp(string, string_with_addr);
}
tests/non-free/strlen.c
+ 246
− 16
View file @ 41235626
This diff is collapsed.
tests/non-free/strnlen2.c 0 → 100644
+ 508
− 0
View file @ 41235626
This diff is collapsed.
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment