diff --git a/ivette/src/dome/renderer/controls/buttons.tsx b/ivette/src/dome/renderer/controls/buttons.tsx
index b42d7cdd14537f4a785054d2f8c31145b90fd6df..1904aa78410d17a45c1e47785e4312d7c8c59946 100644
--- a/ivette/src/dome/renderer/controls/buttons.tsx
+++ b/ivette/src/dome/renderer/controls/buttons.tsx
@@ -498,7 +498,7 @@ export interface SelectProps {
* <option value='…' disabled=… >…</option>
*/
-export function Select(props: SelectProps): JSX.Element {
+export function SelectMenu(props: SelectProps): JSX.Element {
const { onChange, placeholder, focus=false } = props;
const className = classes(
'dome-xSelect dome-xBoxButton dome-xButton-default dome-xButton-label',
diff --git a/ivette/src/dome/renderer/frame/style.css b/ivette/src/dome/renderer/frame/style.css
index 0a7fe9e602bfaaa9d382f549f540babb6c9cb650..44f4580e0f4ad8de3985f0b2f90ef70066a8cd6c 100644
--- a/ivette/src/dome/renderer/frame/style.css
+++ b/ivette/src/dome/renderer/frame/style.css
@@ -505,7 +505,7 @@
overflow-x: hidden;
overflow-y: auto;
max-height: 120px;
- z-index: +1;
+ z-index: +10;
width: 0px;
background: var(--background-alterning-odd);
}
diff --git a/ivette/src/dome/renderer/layout/forms.tsx b/ivette/src/dome/renderer/layout/forms.tsx
index f51f07b8133de2aad17736be2eb298035e04c4a1..bf30fccd8aa229908c3b7def7242991bebf5a2f7 100644
--- a/ivette/src/dome/renderer/layout/forms.tsx
+++ b/ivette/src/dome/renderer/layout/forms.tsx
@@ -43,10 +43,10 @@ import Events from 'events';
import React, { Children } from 'react';
import * as Dome from 'dome';
import * as Utils from 'dome/misc/utils';
-import { Hbox } from 'dome/layout/boxes';
-import { Icon, IconKind, SVG } from 'dome/controls/icons';
-import { Checkbox, Radio, Select as SelectMenu } from 'dome/controls/buttons';
import { Label } from 'dome/controls/labels';
+import { Icon, IconKind, SVG } from 'dome/controls/icons';
+import { Checkbox, Radio, SelectMenu, Button } from 'dome/controls/buttons';
+import { Hbox } from 'dome/layout/boxes';
export type FieldError =
| undefined | boolean | string
@@ -1575,6 +1575,36 @@ export function ColorField(props: ColorFieldProps): JSX.Element {
);
}
+/* --------------------------------------------------------------------------*/
+/* --- Button Field ---*/
+/* --------------------------------------------------------------------------*/
+/** @category Form Fields */
+export function ButtonField(props: FieldProps<boolean>): JSX.Element | null {
+ const { hidden, disabled } = useContext(props);
+
+ if (hidden) return null;
+
+ const { value, onChanged } = props.state;
+ const { label, title } = props;
+ const css = Utils.classes(
+ 'dome-xForm-field dome-text-label',
+ disabled && 'dome-disabled',
+ );
+ const onClick = (): void => {
+ onChanged(!value, undefined, false);
+ };
+ return (
+ <Button
+ className={css}
+ label={label}
+ title={title}
+ disabled={disabled}
+ selected= {value}
+ onClick={onClick}
+ />
+ );
+}
+
/* --------------------------------------------------------------------------*/
/* --- Check Box Field ---*/
/* --------------------------------------------------------------------------*/
diff --git a/ivette/src/frama-c/plugins/eva/DomainStates.tsx b/ivette/src/frama-c/plugins/eva/DomainStates.tsx
index e06725e6f2e002ecc4fc224cadfe451dca10b882..bad51ee797ca495998950b8e4c40b0eb6f1546fc 100644
--- a/ivette/src/frama-c/plugins/eva/DomainStates.tsx
+++ b/ivette/src/frama-c/plugins/eva/DomainStates.tsx
@@ -29,7 +29,7 @@ import * as Eva from 'frama-c/plugins/eva/api/general';
import * as Boxes from 'dome/layout/boxes';
import { HSplit } from 'dome/layout/splitters';
import { Text } from 'frama-c/richtext';
-import { Checkbox, Select } from 'dome/controls/buttons';
+import { Checkbox, SelectMenu } from 'dome/controls/buttons';
import { Label } from 'dome/controls/labels';
const globalSelectedDomain = new GlobalState("");
@@ -73,13 +73,13 @@ export function EvaStates(): JSX.Element {
<>
<Boxes.Hbox className="domain-state-box">
<Label>Domain: </Label>
- <Select
+ <SelectMenu
title="Select the analysis domain to be shown"
value={selected}
onChange={(domain) => setSelected(domain ?? "")}
>
{list}
- </Select>
+ </SelectMenu>
<Boxes.Filler/>
<Checkbox
label="Filtered state"
diff --git a/ivette/src/frama-c/plugins/wp/tac.tsx b/ivette/src/frama-c/plugins/wp/tac.tsx
index cc3f0f786dfd8e22fa7392eb8b1d918e139b61f0..9142ea968db407fc44cfb7df1a19578007f92a90 100644
--- a/ivette/src/frama-c/plugins/wp/tac.tsx
+++ b/ivette/src/frama-c/plugins/wp/tac.tsx
@@ -24,7 +24,7 @@ import React, { Fragment } from 'react';
import { classes } from 'dome/misc/utils';
import { Icon } from 'dome/controls/icons';
import { IconButton, IconButtonKind } from 'dome/controls/buttons';
-import { Spinner, Select } from 'dome/controls/buttons';
+import { Spinner, SelectMenu } from 'dome/controls/buttons';
import { Label, Item, Descr } from 'dome/controls/labels';
import { Hbox, Vbox, Filler } from 'dome/layout/boxes';
import { Separator } from 'dome/frame/toolbars';
@@ -346,12 +346,12 @@ function SelectorParam(props: ParameterProps): JSX.Element
};
return (
<Label label={label} title={title}>
- <Select
+ <SelectMenu
className="wp-config-field wp-config-select"
value={value}
disabled={locked}
onChange={onChange}
- >{options}</Select>
+ >{options}</SelectMenu>
</Label>
);
}
diff --git a/ivette/src/sandbox/qsplit.tsx b/ivette/src/sandbox/qsplit.tsx
index bf6e17598efcac7d38b3217fe9e9cf11fc66a0f4..46918acf7d37589691594af37acb4449d57cb3d0 100644
--- a/ivette/src/sandbox/qsplit.tsx
+++ b/ivette/src/sandbox/qsplit.tsx
@@ -39,14 +39,14 @@ function Quarter(props: {
}): JSX.Element {
const onChange = (s?: string): void => props.setValue(s ? s : undefined);
return (
- <Ctrl.Select value={props.value ?? ''} onChange={onChange}>
+ <Ctrl.SelectMenu value={props.value ?? ''} onChange={onChange}>
<option value=''>-</option>
<option value='A'>A</option>
<option value='B'>B</option>
<option value='C'>C</option>
<option value='D'>D</option>
<option value='E'>E</option>
- </Ctrl.Select>
+ </Ctrl.SelectMenu>
);
}
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 471bf33f62c10109b6778b760901dc5eb19a9dc3..826000ae54ffa9595eedb80f6b79a4ffc35b6861 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -3040,11 +3040,9 @@ let rec collectInitializer
| Some len -> begin
match constFoldToInt len with
| Some ni when Integer.ge ni Integer.zero -> to_integer ni, false
- | _ ->
- abort_context
- "Array length %a is not a compile-time constant: \
- no explicit initializer allowed."
- Cil_printer.pp_exp len
+ | _ -> (* VLA cannot have initializers, and this should have
+ been captured beforehand. *)
+ Kernel.fatal "Trying to initialize a variable-length array"
end
| _ ->
(* unsized array case, length comes from initializers *)
@@ -3980,6 +3978,11 @@ let get_lval_compound_assigned op expr =
Cil_printer.pp_lval x
| _ -> abort_context "Expected lval for %s" op
+type var_decl_kind =
+ [ `FormalDecl | `GlobalDecl | `LocalDecl | `LocalStaticDecl ]
+type type_context =
+ [ var_decl_kind | `FieldDecl | `Typedef | `OnlyType ]
+
(* The way formals are handled now might generate incorrect types, in the
sense that they refer to a varinfo (in the case of VLA depending on a
previously declared formal) that exists only during the call to doType.
@@ -4448,8 +4451,7 @@ let rec doSpecList loc ghost (suggestedAnonName: string)
*)
t'
- | [Cabs.TtypeofT (specs, dt)] ->
- doOnlyType loc ghost specs dt
+ | [Cabs.TtypeofT (specs, dt)] -> doOnlyType loc ghost specs dt
| l ->
abort_context
@@ -4471,21 +4473,22 @@ and convertCVtoAttr (src: Cabs.cvspec list) : Cabs.attribute list =
and makeVarInfoCabs
~(ghost:bool)
- ~(isformal: bool)
- ~(isglobal: bool)
+ ~(kind:var_decl_kind)
?(isgenerated=false)
?(referenced=false)
(ldecl : location)
(bt, sto, inline, attrs)
(n,ndt,a)
: varinfo =
+ let isglobal = kind = `GlobalDecl || kind = `LocalStaticDecl in
+ let isformal = kind = `FormalDecl in
let vtype, nattr =
- doType ghost isformal (AttrName false)
- ~allowVarSizeArrays:isformal (* For locals we handle var-sized arrays
- before makeVarInfoCabs; for formals
- we do it afterwards *)
- bt (Cabs.PARENTYPE(attrs, ndt, a)) in
- (*Format.printf "Got yp:%a->%a(%a)@." d_type bt d_type vtype d_attrlist nattr;*)
+ doType ghost (kind:>type_context) (AttrName false)
+ ~allowVarSizeArrays:isformal
+ (* For locals we handle var-sized arrays before makeVarInfoCabs;
+ Hence, at this point only formals can have a VLA type *)
+ bt (Cabs.PARENTYPE(attrs, ndt, a))
+ in
if hasAttribute "thread" nattr then begin
let wkey = Kernel.wkey_inconsistent_specifier in
let source = fst ldecl in
@@ -4509,17 +4512,13 @@ and makeVarInfoCabs
if inline && not (isFunctionType vtype) then
Kernel.error ~once:true ~current:true "inline for a non-function: %s" n;
checkRestrictQualifierDeep vtype;
- (* log "Looking at %s(%b): (%a)@." n isformal d_attrlist nattr;*)
- let vi = makeVarinfo ~ghost ~referenced ~temp:isgenerated ~loc:ldecl isglobal isformal n vtype
+ let vi =
+ makeVarinfo ~ghost ~referenced ~temp:isgenerated ~loc:ldecl isglobal isformal n vtype
in
vi.vstorage <- sto;
vi.vattr <- nattr;
vi.vdefined <-
not (isFunctionType vtype) && isglobal && (sto = NoStorage || sto = Static);
-
- (* if false then
- log "Created varinfo %s : %a\n" vi.vname d_type vi.vtype;*)
-
vi
(* Process a local variable declaration and allow variable-sized arrays *)
@@ -4527,12 +4526,12 @@ and makeVarSizeVarInfo ghost (ldecl : location)
spec_res
(n,ndt,a)
: varinfo * chunk * exp * bool =
+ let kind = `LocalDecl in
if not (Cil.msvcMode ()) then
match isVariableSizedArray ghost ndt with
| None ->
- makeVarInfoCabs ~ghost ~isformal:false
- ~isglobal:false
- ldecl spec_res (n,ndt,a), empty, zero ~loc:ldecl, false
+ makeVarInfoCabs ~ghost ~kind ldecl spec_res (n,ndt,a),
+ empty, zero ~loc:ldecl, false
| Some (ndt', se, len) ->
(* In this case, we have changed the type from VLA to pointer: add the
qualifier to the elements. *)
@@ -4541,13 +4540,10 @@ and makeVarSizeVarInfo ghost (ldecl : location)
(t, sto , inline , ("ghost", []) :: attrs)
| normal -> normal
in
- makeVarInfoCabs ~ghost ~isformal:false
- ~isglobal:false
- ldecl spec_res (n,ndt',a), se, len, true
+ makeVarInfoCabs ~ghost ~kind ldecl spec_res (n,ndt',a), se, len, true
else
- makeVarInfoCabs ~ghost ~isformal:false
- ~isglobal:false
- ldecl spec_res (n,ndt,a), empty, zero ~loc:ldecl, false
+ makeVarInfoCabs ~ghost ~kind ldecl spec_res (n,ndt,a),
+ empty, zero ~loc:ldecl, false
and doAttr ghost (a: Cabs.attribute) : attribute list =
(* Strip the leading and trailing underscore *)
@@ -4671,9 +4667,7 @@ and cabsPartitionAttributes
in
loop ([], [], []) attrs
-
-
-and doType (ghost:bool) isFuncArg
+and doType (ghost:bool) (context: type_context)
(nameortype: attributeClass) (* This is AttrName if we are doing
* the type for a name, or AttrType
* if we are doing this type in a
@@ -4698,10 +4692,7 @@ and doType (ghost:bool) isFuncArg
let a1n, a1f, a1t = partitionAttributes ~default:AttrType a1' in
let a2' = doAttributes ghost a2 in
let a2n, a2f, a2t = partitionAttributes ~default:nameortype a2' in
- (*Format.printf "doType: @[a1n=%a@\na1f=%a@\na1t=%a@\na2n=%a@\na2f=%a@\na2t=%a@]@\n" d_attrlist a1n d_attrlist a1f d_attrlist a1t d_attrlist a2n d_attrlist a2f d_attrlist a2t;*)
let bt' = cabsTypeAddAttributes a1t bt in
- (* log "bt' = %a@." d_type bt';*)
-
let bt'', a1fadded =
match unrollType bt with
| TFun _ -> cabsTypeAddAttributes a1f bt', true
@@ -4737,7 +4728,6 @@ and doType (ghost:bool) isFuncArg
Cil_printer.pp_attributes a2f;
restyp
in
- (* log "restyp' = %a@." d_type restyp';*)
(* Now add the name attributes and return *)
restyp', cabsAddAttributes a1n (cabsAddAttributes a2n nattr)
@@ -4848,12 +4838,28 @@ and doType (ghost:bool) isFuncArg
"Unable to do constant-folding on array length %a. \
Some CIL operations on this array may fail."
Cil_printer.pp_exp cst
- else
- Kernel.error ~once:true ~current:true
- "Array length %a is not a compile-time constant,@ \
- and currently VLAs may only have their first dimension \
- as variable."
- Cil_printer.pp_exp cst
+ else begin
+ match context with
+ | `FieldDecl ->
+ Kernel.error ~once:true ~current:true
+ "\"Variable length array in structure\" extension \
+ is not supported"
+ | `GlobalDecl ->
+ Kernel.error ~once:true ~current:true
+ "Global arrays cannot have variable size"
+ | `LocalStaticDecl ->
+ Kernel.error ~once:true ~current:true
+ "Static arrays cannot have variable size"
+ | `Typedef ->
+ Kernel.error ~once:true ~current:true
+ "A type definition cannot be a variable-length array"
+ | `LocalDecl ->
+ Kernel.not_yet_implemented
+ "For multi-dimensional arrays, variable length is only \
+ supported on the first dimension"
+ | `OnlyType | `FormalDecl ->
+ Kernel.fatal "VLA should be accepted in this context"
+ end
| _ -> ());
if Cil.isZero len' && not allowZeroSizeArrays &&
not (Cil.gccMode () || Cil.msvcMode ())
@@ -4863,7 +4869,7 @@ and doType (ghost:bool) isFuncArg
Some len'
in
let al' = doAttributes ghost al in
- if not isFuncArg && hasAttribute "static" al' then
+ if context <> `FormalDecl && hasAttribute "static" al' then
Kernel.error ~once:true ~current:true
"static specifier inside array argument is allowed only in \
function argument";
@@ -4900,8 +4906,9 @@ and doType (ghost:bool) isFuncArg
let doOneArg argl_length is_ghost (s, (n, ndt, a, cloc)) : varinfo =
let ghost = is_ghost || ghost in
let s' = doSpecList cloc ghost n s in
- let vi = makeVarInfoCabs ~ghost ~isformal:true ~isglobal:false
- (convLoc cloc) s' (n,ndt,a) in
+ let vi =
+ makeVarInfoCabs ~ghost ~kind:`FormalDecl (convLoc cloc) s' (n,ndt,a)
+ in
if isVoidType vi.vtype then begin
if argl_length > 1 then
Kernel.error ~once:true ~current:true
@@ -5057,12 +5064,14 @@ and isVariableSizedArray ghost (dt: Cabs.decl_type)
| None -> None
| Some (se, e) -> Some (dt', se, e)
-and doOnlyType loc ghost (specs: Cabs.spec_elem list) (dt: Cabs.decl_type) : typ =
+and doOnlyType loc ghost specs dt =
let bt',sto,inl,attrs = doSpecList loc ghost "" specs in
if sto <> NoStorage || inl then
Kernel.error ~once:true ~current:true "Storage or inline specifier in type only";
let tres, nattr =
- doType ghost false AttrType bt' (Cabs.PARENTYPE(attrs, dt, [])) in
+ doType ghost `OnlyType AttrType bt' (Cabs.PARENTYPE(attrs, dt, []))
+ ~allowVarSizeArrays:true
+ in
if nattr <> [] then
Kernel.error ~once:true ~current:true
"Name attributes in only_type: %a" Cil_printer.pp_attributes nattr;
@@ -5106,7 +5115,7 @@ and makeCompType loc ghost (isstruct: bool)
let allowZeroSizeArrays = Cil.gccMode () || Cil.msvcMode () in
let ftype, fattr =
doType
- ~allowZeroSizeArrays ghost false (AttrName false) bt
+ ~allowZeroSizeArrays ghost `FieldDecl (AttrName false) bt
(Cabs.PARENTYPE(attrs, ndt, a))
in
(* check for fields whose type is incomplete. In particular, this rules
@@ -8497,8 +8506,10 @@ and createGlobal loc ghost logic_spec ((t,s,b,attr_list) : (typ * storage * bool
in
(* Make a first version of the varinfo *)
let vi_loc = convLoc cloc in
- let vi = makeVarInfoCabs ~ghost ~isformal:false ~referenced:islibc
- ~isglobal:true ~isgenerated vi_loc (t,s,b,attr_list) (n,ndt,a)
+ let vi =
+ makeVarInfoCabs
+ ~ghost ~kind:`GlobalDecl ~referenced:islibc ~isgenerated
+ vi_loc (t,s,b,attr_list) (n,ndt,a)
in
(* Add the variable to the environment before doing the initializer
* because it might refer to the variable itself *)
@@ -8784,9 +8795,8 @@ and createLocal ghost ((_, sto, _, _) as specs)
in
let newname, _ = newAlphaName ghost true "" full_name in
(* Make it global *)
- let vi = makeVarInfoCabs ~ghost ~isformal:false
- ~isglobal:true
- loc specs (n, ndt, a) in
+ let vi = makeVarInfoCabs ~ghost ~kind:`LocalStaticDecl loc specs (n, ndt, a)
+ in
checkArray inite vi;
vi.vname <- newname;
let attrs = Cil.addAttribute (Attr (fc_local_static,[])) vi.vattr in
@@ -8867,8 +8877,7 @@ and createLocal ghost ((_, sto, _, _) as specs)
let savelen =
makeVarInfoCabs
~ghost
- ~isformal:false
- ~isglobal:false
+ ~kind:`LocalDecl
loc
(theMachine.typeOfSizeOf, NoStorage, false, [])
("__lengthof_" ^ vi.vname,JUSTBASE, [])
@@ -9078,7 +9087,7 @@ and doDecl local_env (isglobal: bool) (def: Cabs.definition) : chunk =
if isglobal then begin
let bt,_,_,attrs = spec_res in
let vtype, nattr =
- doType local_env.is_ghost false
+ doType local_env.is_ghost `GlobalDecl
(AttrName false) bt (Cabs.PARENTYPE(attrs, ndt, a)) in
(match filterAttributes "alias" nattr with
| [] -> (* ordinary prototype. *)
@@ -9216,8 +9225,9 @@ and doDecl local_env (isglobal: bool) (def: Cabs.definition) : chunk =
let bt,sto,inl,attrs = doSpecList idloc local_env.is_ghost n specs in
!currentFunctionFDEC.svar.vinline <- inl;
let ftyp, funattr =
- doType local_env.is_ghost false
- (AttrName false) bt (Cabs.PARENTYPE(attrs, dt, a)) in
+ doType local_env.is_ghost `GlobalDecl
+ (AttrName false) bt (Cabs.PARENTYPE(attrs, dt, a))
+ in
if hasAttribute "thread" funattr then begin
let wkey = Kernel.wkey_inconsistent_specifier in
let source = fst funloc in
@@ -9621,7 +9631,7 @@ and doTypedef ghost ((specs, nl): Cabs.name_group) =
let createTypedef ((n,ndt,a,_) : Cabs.name) =
(* E.s (error "doTypeDef") *)
let newTyp, tattr =
- doType ghost false AttrType bt (Cabs.PARENTYPE(attrs, ndt, a)) in
+ doType ghost `Typedef AttrType bt (Cabs.PARENTYPE(attrs, ndt, a)) in
checkTypedefSize n newTyp;
let tattr = fc_stdlib_attribute tattr in
let newTyp' = cabsTypeAddAttributes tattr newTyp in
@@ -9720,7 +9730,7 @@ and doOnlyTypedef ghost (specs: Cabs.spec_elem list) : unit =
Kernel.error ~once:true ~current:true
"Storage or inline specifier not allowed in typedef";
let restyp, nattr =
- doType ghost false AttrType bt (Cabs.PARENTYPE(attrs, Cabs.JUSTBASE, []))
+ doType ghost `Typedef AttrType bt (Cabs.PARENTYPE(attrs, Cabs.JUSTBASE, []))
in
if nattr <> [] then
Kernel.warning ~current:true "Ignoring identifier attribute";
@@ -10237,7 +10247,7 @@ and doStatement local_env (s : Cabs.statement) : chunk =
let spec = doSpecList ldecl ghost n t in
let vi =
makeVarInfoCabs
- ~ghost ~isformal:false ~isglobal:false ldecl spec (n,ndt,a)
+ ~ghost ~kind:`LocalDecl ldecl spec (n,ndt,a)
in
addLocalToEnv ghost n (EnvVar vi);
!currentFunctionFDEC.slocals <- vi :: !currentFunctionFDEC.slocals;
diff --git a/src/plugins/eva/domains/cvalue/builtins_memory.ml b/src/plugins/eva/domains/cvalue/builtins_memory.ml
index dc8645d225f1c589193e248a2f98772f4f28e95d..f0c86e9e19d7f609b5eb98ddc2a6283a925be82d 100644
--- a/src/plugins/eva/domains/cvalue/builtins_memory.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_memory.ml
@@ -31,12 +31,24 @@ let register_builtin name ?replace builtin =
let dkey = Self.register_category "imprecision"
-let rec lval_of_address exp =
+let rec pretty_lval_of_address exp =
match exp.node with
| AddrOf lval -> lval
- | CastE (_typ, exp) -> lval_of_address exp
+ | CastE (_typ, exp) when Cil.isPointerType exp.typ ->
+ (* Removes conversion to void* for more readable messages. *)
+ pretty_lval_of_address exp
| _ -> Eva_ast.Build.mem exp
+let warn_imprecise_offsm_write ~name dst_expr offsetmap =
+ let prefix = "Builtin " ^ name in
+ let dst_lval = pretty_lval_of_address dst_expr in
+ Cvalue_transfer.warn_imprecise_offsm_write ~prefix dst_lval offsetmap
+
+let warn_imprecise_write ~name dst_expr loc v =
+ let prefix = "Builtin " ^ name in
+ let dst_lval = pretty_lval_of_address dst_expr in
+ Cvalue_transfer.warn_imprecise_write ~prefix dst_lval loc v
+
let plevel = Parameters.ArrayPrecisionLevel.get
(* Create a dependency [\from arg_n] where n is the nth argument of the
@@ -95,13 +107,12 @@ let add_sure_deps ~size ~src ~dst (deps_table, sure_output) =
deps_table, Zone.join sure_zone sure_output
(* Copy the offsetmap of size [size] from [src] to [dst] in [state]. *)
-let copy_offsetmap ~name ~exact ~size ~src ~dst ~dst_lval state =
+let copy_offsetmap ~name ~exact ~size ~src ~dst ~dst_expr state =
match Cvalue.Model.copy_offsetmap src size state with
| `Bottom -> Cvalue.Model.bottom
| `Value offsetmap ->
check_indeterminate_offsetmap ~name offsetmap;
- let prefix = "Builtin " ^ name in
- Cvalue_transfer.warn_imprecise_offsm_write ~prefix dst_lval offsetmap;
+ warn_imprecise_offsm_write ~name dst_expr offsetmap;
Cvalue.Model.paste_offsetmap ~from:offsetmap ~dst_loc:dst ~size ~exact state
(* Returns the min and max size of a copy from an Ival.t. *)
@@ -125,7 +136,7 @@ let shift ~factor:i src dst size =
after the copy for the minimum size has already been done.
Iterates on all possible values of [size] (after the first), and does the
copy for [previous_size..size]. *)
-let copy_remaining_size_by_size ~name ~src ~dst ~dst_lval ~size state =
+let copy_remaining_size_by_size ~name ~src ~dst ~dst_expr ~size state =
let exception Result of Cvalue.Model.t in
let do_size size (state, previous_size) =
(* First iteration: this copy has already been performed, skip. *)
@@ -137,7 +148,7 @@ let copy_remaining_size_by_size ~name ~src ~dst ~dst_lval ~size state =
(* [exact] is false as all these copies may not happen according to the
concrete value of [size]. *)
let exact = false in
- let new_state = copy_offsetmap ~name ~exact ~size ~src ~dst ~dst_lval state in
+ let new_state = copy_offsetmap ~name ~exact ~size ~src ~dst ~dst_expr state in
(* If this copy failed, the current size is completely invalid, and so
will be the following ones. Stop now with the previous state. *)
if not (Cvalue.Model.is_reachable new_state) then raise (Result state);
@@ -147,7 +158,7 @@ let copy_remaining_size_by_size ~name ~src ~dst ~dst_lval ~size state =
with Result state -> state
(* Copy the value at location [src_loc] to location [dst_loc] in [state]. *)
-let imprecise_copy ~name ~src_loc ~dst_loc ~dst_lval state =
+let imprecise_copy ~name ~src_loc ~dst_loc ~dst_expr state =
Self.debug ~dkey ~once:true ~current:true
"In %s builtin: too many sizes to enumerate, possible loss of precision"
name;
@@ -155,8 +166,7 @@ let imprecise_copy ~name ~src_loc ~dst_loc ~dst_lval state =
let v = Model.find_indeterminate ~conflate_bottom:false state src_loc in
warn_indeterminate_value ~name v;
let value = Cvalue.V_Or_Uninitialized.get_v v in
- let prefix = "Builtin " ^ name in
- Cvalue_transfer.warn_imprecise_write ~prefix dst_lval dst_loc value;
+ warn_imprecise_write ~name dst_expr dst_loc value;
let new_state =
Cvalue.Model.add_indeterminate_binding ~exact:false state dst_loc v
in
@@ -177,7 +187,7 @@ let char_location loc max_size =
let loc = Location_Bits.shift shift loc in
make_loc loc (Int_Base.inject size_char)
-let compute_memcpy ~name ~dst_lval ~dst ~src ~size state =
+let compute_memcpy ~name ~dst_expr ~dst ~src ~size state =
let size_min, size_max = min_max_size size in
(* Empty \from dependencies and sure output *)
let empty_deps = Assigns.Memory.empty, Zone.bottom in
@@ -187,7 +197,7 @@ let compute_memcpy ~name ~dst_lval ~dst ~src ~size state =
if Int.gt size_min Int.zero
then
let state =
- copy_offsetmap ~name ~exact:true ~size:size_min ~src ~dst ~dst_lval state
+ copy_offsetmap ~name ~exact:true ~size:size_min ~src ~dst ~dst_expr state
in
(* If the copy succeeded, update \from dependencies and sure output. *)
if Cvalue.Model.is_reachable state
@@ -213,15 +223,14 @@ let compute_memcpy ~name ~dst_lval ~dst ~src ~size state =
write the result as one byte in dst+(size_min..size_max-1). *)
let state =
if Ival.cardinal_is_less_than size (plevel () / 10)
- then copy_remaining_size_by_size ~name ~src ~dst ~dst_lval ~size state
- else imprecise_copy ~name ~src_loc ~dst_loc ~dst_lval state
+ then copy_remaining_size_by_size ~name ~src ~dst ~dst_expr ~size state
+ else imprecise_copy ~name ~src_loc ~dst_loc ~dst_expr state
in
state, deps_table, written_zone
let frama_c_memcpy name state actuals =
match actuals with
- | [(dst_exp, dst_cvalue); (_src_exp, src_cvalue); (_size_exp, size_cvalue)] ->
- let dst_lval = lval_of_address dst_exp in
+ | [(dst_expr, dst_cvalue); (_src_exp, src_cvalue); (_size_exp, size_cvalue)] ->
let size =
try Cvalue.V.project_ival size_cvalue
with Cvalue.V.Not_based_on_null -> Ival.top (* TODO: use size_t *)
@@ -235,7 +244,7 @@ let frama_c_memcpy name state actuals =
let dst = reduce_to_valid_loc dst size Locations.Write in
(* Do the copy. *)
let state, memory, sure_output =
- compute_memcpy ~name ~dst_lval ~dst ~src ~size state
+ compute_memcpy ~name ~dst_expr ~dst ~src ~size state
in
(* Build the builtin results. *)
let return = deps_nth_arg 0 in
@@ -260,15 +269,14 @@ let () =
(* -------------------------------------------------------------------------- *)
(* Implementation of [memset] that accepts imprecise arguments. *)
-let frama_c_memset_imprecise state dst_lval dst v size =
- let prefix = "Builtin memset" in
+let frama_c_memset_imprecise state dst_expr dst v size =
let size_min, size_max = min_max_size size in
(* Write [v] everywhere that might be written, ie between
[dst] and [dst+size-1]. *)
let state, over_zone =
if Int.gt size_max Int.zero then
let loc = char_location dst size_max in
- Cvalue_transfer.warn_imprecise_write ~prefix dst_lval loc v;
+ warn_imprecise_write ~name:"memset" dst_expr loc v;
let state = Cvalue.Model.add_binding ~exact:false state loc v in
let written_zone = enumerate_valid_bits Locations.Write loc in
state, written_zone
@@ -289,7 +297,7 @@ let frama_c_memset_imprecise state dst_lval dst v size =
let vuninit = V_Or_Uninitialized.initialized v in
let size_v = Bit_utils.sizeofchar () in
let from = V_Offsetmap.create ~size:sure vuninit ~size_v in
- Cvalue_transfer.warn_imprecise_offsm_write ~prefix dst_lval from;
+ warn_imprecise_offsm_write ~name:"memset" dst_expr from;
let state =
Cvalue.Model.paste_offsetmap
~from ~dst_loc ~size:sure ~exact:true state
@@ -452,7 +460,7 @@ let memset_typ_offsm typ v =
(* Precise memset builtin, that requires its arguments to be sufficiently
precise abstract values. *)
-let frama_c_memset_precise state dst_lval dst v (exp_size, size) =
+let frama_c_memset_precise state dst_expr dst v (exp_size, size) =
try
(* We want an exact size, Otherwise, we can use the imprecise memset as a
fallback *)
@@ -483,8 +491,7 @@ let frama_c_memset_precise state dst_lval dst v (exp_size, size) =
snd (Bit_utils.(find_offset vi_dst.vtype ~offset mo))
in
let offsm = memset_typ_offsm typ v in
- let prefix = "Builtin memset" in
- Cvalue_transfer.warn_imprecise_offsm_write ~prefix dst_lval offsm;
+ warn_imprecise_offsm_write ~name:"memset" dst_expr offsm;
let state =
Cvalue.Model.paste_offsetmap
~from:offsm ~dst_loc:dst ~size ~exact:true state
@@ -503,9 +510,8 @@ let frama_c_memset_precise state dst_lval dst v (exp_size, size) =
let frama_c_memset state actuals =
match actuals with
- | [(dst_exp, dst_cvalue); (_, v); (exp_size, size_cvalue)] ->
+ | [(dst_expr, dst_cvalue); (_, v); (exp_size, size_cvalue)] ->
begin
- let dst_lval = lval_of_address dst_exp in
let size =
try Cvalue.V.project_ival size_cvalue
with Cvalue.V.Not_based_on_null -> Ival.top (* TODO: use size_t *)
@@ -523,13 +529,13 @@ let frama_c_memset state actuals =
v
in
let state, sure_output, over_output =
- try frama_c_memset_precise state dst_lval dst v (exp_size, size)
+ try frama_c_memset_precise state dst_expr dst v (exp_size, size)
with ImpreciseMemset reason ->
Self.debug ~dkey ~current:true
"Call to builtin precise_memset(%a) failed; %s%t"
Eva_utils.pretty_actuals actuals (imprecision_descr reason)
Eva_utils.pp_callstack;
- frama_c_memset_imprecise state dst_lval dst v size
+ frama_c_memset_imprecise state dst_expr dst v size
in
let assigns =
let value_dep = deps_nth_arg 1 in
diff --git a/tests/builtins/memcpy.c b/tests/builtins/memcpy.c
index ef418d90402f55388a6f9088619cd2963e6cfa19..1eee41ee76b0945dee477cf8f5602de8761e015a 100644
--- a/tests/builtins/memcpy.c
+++ b/tests/builtins/memcpy.c
@@ -1,7 +1,9 @@
/* run.config*
- PLUGIN: @PTEST_PLUGIN@ report
- STDOPT: +"-calldeps -eva-slevel-function init:2000 -eva-msg-key imprecision -eva-plevel 150 -main main_all -inout -no-deps -absolute-valid-range 100000-100001 -then -report"
+ PLUGIN: @PTEST_PLUGIN@ report
+ STDOPT: +"-calldeps -eva-msg-key imprecision -eva-plevel 150 -inout -no-deps -then -report"
+ STDOPT: +"-absolute-valid-range 100000-100001 -main copy_0"
*/
+
#include "string.h"
volatile int i;
@@ -10,6 +12,7 @@ char dst1[20], dst2[20], dst3[20], dst4[20], dst5[100];
void init () {
int j;
+ //@ loop unroll 20;
for (j=0;j<20;j++) {
src[j] = j+1;
dst1[j] = -1;
@@ -17,6 +20,7 @@ void init () {
dst3[j] = -1;
dst4[j] = -1;
}
+ //@ loop unroll 100;
for (j=0;j<100;j++) dst5[j] = -1;
}
@@ -57,7 +61,7 @@ struct t1 { int x; int y; int* p; char padding[24];} v1,v2, v3, v4, v5;
struct t1 t[4];
-void main (int a, int b){
+void test (int a, int b){
buggy ();
many ();
@@ -94,7 +98,7 @@ void main (int a, int b){
int x=1;
while(1)
memcpy((void *)&x, (void const*)&x, i);
- }
+ }
char *p;
p = maybe ? &dst5[0] : &dst5[20];
@@ -164,7 +168,7 @@ int itv(int l, int u);
*/
void make_unknown(unsigned char *p, size_t l);
-void main_uninit () {
+void test_uninit () {
unsigned char a[50];
unsigned char b[50];
int r = 0;
@@ -202,7 +206,7 @@ void main_uninit () {
}
}
-void main_local() {
+void test_local() {
int* p, *q;
{ int y;
q = &y;
@@ -213,19 +217,16 @@ void main_local() {
}
void copy_0() {
-
-
-
int l;
if (i) memcpy(0, &l, 0);
if (i) memcpy(&l, 0, 0);
}
-void main_all () {
- if (maybe) main (maybe, maybe);
- else if (maybe) main_uninit ();
- else if (maybe) main_local ();
+void main () {
+ if (maybe) test (maybe, maybe);
+ else if (maybe) test_uninit ();
+ else if (maybe) test_local ();
else if (maybe) copy_0 ();
while (1); // results of main are unimportant
}
diff --git a/tests/builtins/oracle/memcpy.res.oracle b/tests/builtins/oracle/memcpy.0.res.oracle
similarity index 77%
rename from tests/builtins/oracle/memcpy.res.oracle
rename to tests/builtins/oracle/memcpy.0.res.oracle
index 7d949b4911c4732f7bc7a8206a5ebdb5aaf85692..774d89fc40dda7ca63cd40f7fe7644081a2a7b0e 100644
--- a/tests/builtins/oracle/memcpy.res.oracle
+++ b/tests/builtins/oracle/memcpy.0.res.oracle
@@ -1,9 +1,8 @@
[kernel] Parsing memcpy.c (with preprocessing)
-[eva] Analyzing a complete application starting at main_all
+[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
- NULL[rbits 800000 to 800015] ∈ [--..--]
i ∈ [--..--]
src[0..19] ∈ {0}
dst1[0..19] ∈ {0}
@@ -21,306 +20,305 @@
v4 ∈ {0}
v5 ∈ {0}
t[0..3] ∈ {0}
-[eva] computing for function main <- main_all.
- Called from memcpy.c:226.
-[eva] computing for function buggy <- main <- main_all.
- Called from memcpy.c:61.
-[eva] memcpy.c:28: Call to builtin memcpy
-[eva:alarm] memcpy.c:28: Warning:
+[eva] computing for function test <- main.
+ Called from memcpy.c:227.
+[eva] computing for function buggy <- test <- main.
+ Called from memcpy.c:65.
+[eva] memcpy.c:32: Call to builtin memcpy
+[eva:alarm] memcpy.c:32: Warning:
function memcpy: precondition 'valid_dest' got status unknown.
-[eva] memcpy.c:28: function memcpy: precondition 'valid_src' got status valid.
-[eva] memcpy.c:28: function memcpy: precondition 'separation' got status valid.
+[eva] memcpy.c:32: function memcpy: precondition 'valid_src' got status valid.
+[eva] memcpy.c:32: function memcpy: precondition 'separation' got status valid.
[eva] FRAMAC_SHARE/libc/string.h:118:
cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp
[eva] Recording results for buggy
[from] Computing for function buggy
[from] Done for function buggy
[eva] Done for function buggy
-[eva] computing for function many <- main <- main_all.
- Called from memcpy.c:63.
-[eva:alarm] memcpy.c:44: Warning: assertion got status unknown.
-[eva] memcpy.c:47: Call to builtin memcpy
-[eva] memcpy.c:47: function memcpy: precondition 'valid_dest' got status valid.
-[eva] memcpy.c:47: function memcpy: precondition 'valid_src' got status valid.
-[eva] memcpy.c:47: function memcpy: precondition 'separation' got status valid.
-[kernel] memcpy.c:47: too many locations to update in array. Approximating.
-[eva] memcpy.c:49: Call to builtin memcpy
-[eva] memcpy.c:49: function memcpy: precondition 'valid_dest' got status valid.
-[eva] memcpy.c:49: function memcpy: precondition 'valid_src' got status valid.
-[eva] memcpy.c:49: function memcpy: precondition 'separation' got status valid.
-[kernel] memcpy.c:49: too many locations to update in array. Approximating.
-[kernel] memcpy.c:49:
- more than 150(1000) locations to update in array. Approximating.
-[kernel] memcpy.c:49: more than 150(1000) elements to enumerate. Approximating.
+[eva] computing for function many <- test <- main.
+ Called from memcpy.c:67.
+[eva:alarm] memcpy.c:48: Warning: assertion got status unknown.
+[eva] memcpy.c:51: Call to builtin memcpy
+[eva] memcpy.c:51: function memcpy: precondition 'valid_dest' got status valid.
+[eva] memcpy.c:51: function memcpy: precondition 'valid_src' got status valid.
+[eva] memcpy.c:51: function memcpy: precondition 'separation' got status valid.
+[kernel] memcpy.c:51: too many locations to update in array. Approximating.
[eva] memcpy.c:53: Call to builtin memcpy
[eva] memcpy.c:53: function memcpy: precondition 'valid_dest' got status valid.
[eva] memcpy.c:53: function memcpy: precondition 'valid_src' got status valid.
[eva] memcpy.c:53: function memcpy: precondition 'separation' got status valid.
[kernel] memcpy.c:53: too many locations to update in array. Approximating.
+[kernel] memcpy.c:53:
+ more than 150(1000) locations to update in array. Approximating.
+[kernel] memcpy.c:53: more than 150(1000) elements to enumerate. Approximating.
+[eva] memcpy.c:57: Call to builtin memcpy
+[eva] memcpy.c:57: function memcpy: precondition 'valid_dest' got status valid.
+[eva] memcpy.c:57: function memcpy: precondition 'valid_src' got status valid.
+[eva] memcpy.c:57: function memcpy: precondition 'separation' got status valid.
+[kernel] memcpy.c:57: too many locations to update in array. Approximating.
[eva] Recording results for many
[from] Computing for function many
[from] Done for function many
[eva] Done for function many
-[eva] computing for function init <- main <- main_all.
- Called from memcpy.c:65.
-[eva] memcpy.c:20: Trace partitioning superposing up to 100 states
+[eva] computing for function init <- test <- main.
+ Called from memcpy.c:69.
+[eva] memcpy.c:24: Trace partitioning superposing up to 100 states
[eva] Recording results for init
[from] Computing for function init
[from] Done for function init
[eva] Done for function init
-[eva:alarm] memcpy.c:67: Warning: assertion got status unknown.
-[eva] memcpy.c:68: Call to builtin memcpy
-[eva] memcpy.c:68: function memcpy: precondition 'valid_dest' got status valid.
-[eva] memcpy.c:68: function memcpy: precondition 'valid_src' got status valid.
-[eva] memcpy.c:68: function memcpy: precondition 'separation' got status valid.
-[eva] memcpy.c:70: Call to builtin memcpy
-[eva:alarm] memcpy.c:70: Warning:
+[eva:alarm] memcpy.c:71: Warning: assertion got status unknown.
+[eva] memcpy.c:72: Call to builtin memcpy
+[eva] memcpy.c:72: function memcpy: precondition 'valid_dest' got status valid.
+[eva] memcpy.c:72: function memcpy: precondition 'valid_src' got status valid.
+[eva] memcpy.c:72: function memcpy: precondition 'separation' got status valid.
+[eva] memcpy.c:74: Call to builtin memcpy
+[eva:alarm] memcpy.c:74: Warning:
function memcpy: precondition 'valid_dest' got status unknown.
-[eva:alarm] memcpy.c:70: Warning:
+[eva:alarm] memcpy.c:74: Warning:
function memcpy: precondition 'valid_src' got status unknown.
-[eva] memcpy.c:70: function memcpy: precondition 'separation' got status valid.
-[eva:alarm] memcpy.c:72: Warning: assertion got status unknown.
-[eva] memcpy.c:73: Call to builtin memcpy
-[eva] memcpy.c:73: function memcpy: precondition 'valid_dest' got status valid.
-[eva] memcpy.c:73: function memcpy: precondition 'valid_src' got status valid.
-[eva] memcpy.c:73: function memcpy: precondition 'separation' got status valid.
-[eva] memcpy.c:75: Call to builtin memcpy
-[eva:alarm] memcpy.c:75: Warning:
+[eva] memcpy.c:74: function memcpy: precondition 'separation' got status valid.
+[eva:alarm] memcpy.c:76: Warning: assertion got status unknown.
+[eva] memcpy.c:77: Call to builtin memcpy
+[eva] memcpy.c:77: function memcpy: precondition 'valid_dest' got status valid.
+[eva] memcpy.c:77: function memcpy: precondition 'valid_src' got status valid.
+[eva] memcpy.c:77: function memcpy: precondition 'separation' got status valid.
+[eva] memcpy.c:79: Call to builtin memcpy
+[eva:alarm] memcpy.c:79: Warning:
function memcpy: precondition 'valid_dest' got status unknown.
-[eva:alarm] memcpy.c:75: Warning:
+[eva:alarm] memcpy.c:79: Warning:
function memcpy: precondition 'valid_src' got status unknown.
-[eva] memcpy.c:75: function memcpy: precondition 'separation' got status valid.
-[eva] memcpy.c:83: Call to builtin memcpy
-[eva] memcpy.c:83: function memcpy: precondition 'valid_dest' got status valid.
-[eva] memcpy.c:83: function memcpy: precondition 'valid_src' got status valid.
-[eva] memcpy.c:83: function memcpy: precondition 'separation' got status valid.
-[eva] memcpy.c:85: Call to builtin memcpy
-[eva] memcpy.c:85: function memcpy: precondition 'valid_dest' got status valid.
-[eva] memcpy.c:85: function memcpy: precondition 'valid_src' got status valid.
-[eva] memcpy.c:85: function memcpy: precondition 'separation' got status valid.
-[eva:alarm] memcpy.c:87: Warning:
+[eva] memcpy.c:79: function memcpy: precondition 'separation' got status valid.
+[eva] memcpy.c:87: Call to builtin memcpy
+[eva] memcpy.c:87: function memcpy: precondition 'valid_dest' got status valid.
+[eva] memcpy.c:87: function memcpy: precondition 'valid_src' got status valid.
+[eva] memcpy.c:87: function memcpy: precondition 'separation' got status valid.
+[eva] memcpy.c:89: Call to builtin memcpy
+[eva] memcpy.c:89: function memcpy: precondition 'valid_dest' got status valid.
+[eva] memcpy.c:89: function memcpy: precondition 'valid_src' got status valid.
+[eva] memcpy.c:89: function memcpy: precondition 'separation' got status valid.
+[eva:alarm] memcpy.c:91: Warning:
pointer downcast. assert (unsigned int)((struct t1 *)t) ≤ 2147483647;
-[eva:garbled-mix:write] memcpy.c:87:
+[eva:garbled-mix:write] memcpy.c:91:
Assigning imprecise value to src
because of arithmetic operation on addresses.
-[eva] memcpy.c:87: Call to builtin memcpy
-[eva] memcpy.c:87: function memcpy: precondition 'valid_dest' got status valid.
-[eva:alarm] memcpy.c:87: Warning:
+[eva] memcpy.c:91: Call to builtin memcpy
+[eva] memcpy.c:91: function memcpy: precondition 'valid_dest' got status valid.
+[eva:alarm] memcpy.c:91: Warning:
function memcpy: precondition 'valid_src' got status unknown.
-[eva] memcpy.c:87: function memcpy: precondition 'separation' got status valid.
-[eva:garbled-mix:write] memcpy.c:87:
+[eva] memcpy.c:91: function memcpy: precondition 'separation' got status valid.
+[eva:garbled-mix:write] memcpy.c:91:
Builtin memcpy: assigning imprecise value to v3
because of misaligned read of addresses.
-[eva:alarm] memcpy.c:89: Warning:
+[eva:alarm] memcpy.c:93: Warning:
pointer downcast. assert (unsigned int)(&v4) ≤ 2147483647;
-[eva:garbled-mix:write] memcpy.c:89:
+[eva:garbled-mix:write] memcpy.c:93:
Assigning imprecise value to dest
because of arithmetic operation on addresses.
-[eva] memcpy.c:89: Call to builtin memcpy
-[eva:alarm] memcpy.c:89: Warning:
+[eva] memcpy.c:93: Call to builtin memcpy
+[eva:alarm] memcpy.c:93: Warning:
function memcpy: precondition 'valid_dest' got status unknown.
-[eva] memcpy.c:89: function memcpy: precondition 'valid_src' got status valid.
-[eva] memcpy.c:89: function memcpy: precondition 'separation' got status valid.
-[eva:alarm] memcpy.c:90: Warning:
+[eva] memcpy.c:93: function memcpy: precondition 'valid_src' got status valid.
+[eva] memcpy.c:93: function memcpy: precondition 'separation' got status valid.
+[eva:alarm] memcpy.c:94: Warning:
pointer downcast. assert (unsigned int)((struct t1 *)t) ≤ 2147483647;
-[eva:alarm] memcpy.c:91: Warning:
+[eva:alarm] memcpy.c:95: Warning:
pointer downcast. assert (unsigned int)(&v5) ≤ 2147483647;
-[eva:garbled-mix:write] memcpy.c:91:
+[eva:garbled-mix:write] memcpy.c:95:
Assigning imprecise value to dest
because of arithmetic operation on addresses.
-[eva] memcpy.c:91: Call to builtin memcpy
-[eva:alarm] memcpy.c:91: Warning:
+[eva] memcpy.c:95: Call to builtin memcpy
+[eva:alarm] memcpy.c:95: Warning:
function memcpy: precondition 'valid_dest' got status unknown.
-[eva] memcpy.c:91: function memcpy: precondition 'valid_src' got status valid.
-[eva] memcpy.c:91: function memcpy: precondition 'separation' got status valid.
-[eva] memcpy.c:96: Call to builtin memcpy
-[eva:alarm] memcpy.c:96: Warning:
+[eva] memcpy.c:95: function memcpy: precondition 'valid_src' got status valid.
+[eva] memcpy.c:95: function memcpy: precondition 'separation' got status valid.
+[eva] memcpy.c:100: Call to builtin memcpy
+[eva:alarm] memcpy.c:100: Warning:
function memcpy: precondition 'valid_dest' got status unknown.
-[eva:alarm] memcpy.c:96: Warning:
+[eva:alarm] memcpy.c:100: Warning:
function memcpy: precondition 'valid_src' got status unknown.
-[eva:alarm] memcpy.c:96: Warning:
+[eva:alarm] memcpy.c:100: Warning:
function memcpy: precondition 'separation' got status unknown.
-[eva:imprecision] memcpy.c:96:
+[eva:imprecision] memcpy.c:100:
In memcpy builtin: too many sizes to enumerate, possible loss of precision
-[eva] memcpy.c:95: starting to merge loop iterations
-[eva] memcpy.c:96: Call to builtin memcpy
-[eva] memcpy.c:101: Call to builtin memcpy
-[eva] memcpy.c:101: function memcpy: precondition 'valid_dest' got status valid.
-[eva] memcpy.c:101: function memcpy: precondition 'valid_src' got status valid.
-[eva] memcpy.c:101: function memcpy: precondition 'separation' got status valid.
-[eva:alarm] memcpy.c:103: Warning: assertion got status unknown.
+[eva] memcpy.c:99: starting to merge loop iterations
+[eva] memcpy.c:100: Call to builtin memcpy
[eva] memcpy.c:105: Call to builtin memcpy
[eva] memcpy.c:105: function memcpy: precondition 'valid_dest' got status valid.
[eva] memcpy.c:105: function memcpy: precondition 'valid_src' got status valid.
[eva] memcpy.c:105: function memcpy: precondition 'separation' got status valid.
-[eva:imprecision] memcpy.c:105:
+[eva:alarm] memcpy.c:107: Warning: assertion got status unknown.
+[eva] memcpy.c:109: Call to builtin memcpy
+[eva] memcpy.c:109: function memcpy: precondition 'valid_dest' got status valid.
+[eva] memcpy.c:109: function memcpy: precondition 'valid_src' got status valid.
+[eva] memcpy.c:109: function memcpy: precondition 'separation' got status valid.
+[eva:imprecision] memcpy.c:109:
In memcpy builtin: too many sizes to enumerate, possible loss of precision
-[eva] memcpy.c:110: starting to merge loop iterations
-[eva] memcpy.c:114: Call to builtin memcpy
-[eva:alarm] memcpy.c:114: Warning:
+[eva] memcpy.c:114: starting to merge loop iterations
+[eva] memcpy.c:118: Call to builtin memcpy
+[eva:alarm] memcpy.c:118: Warning:
function memcpy: precondition 'valid_dest' got status unknown.
-[eva] memcpy.c:114: function memcpy: precondition 'valid_src' got status valid.
-[eva] memcpy.c:114: function memcpy: precondition 'separation' got status valid.
-[kernel] memcpy.c:114: too many locations to update in array. Approximating.
-[eva] memcpy.c:118: starting to merge loop iterations
-[eva] memcpy.c:122: Call to builtin memcpy
-[eva:alarm] memcpy.c:122: Warning:
+[eva] memcpy.c:118: function memcpy: precondition 'valid_src' got status valid.
+[eva] memcpy.c:118: function memcpy: precondition 'separation' got status valid.
+[kernel] memcpy.c:118: too many locations to update in array. Approximating.
+[eva] memcpy.c:122: starting to merge loop iterations
+[eva] memcpy.c:126: Call to builtin memcpy
+[eva:alarm] memcpy.c:126: Warning:
function memcpy: precondition 'valid_dest' got status unknown.
-[eva] memcpy.c:122: function memcpy: precondition 'valid_src' got status valid.
-[eva] memcpy.c:122: function memcpy: precondition 'separation' got status valid.
-[kernel] memcpy.c:122: too many locations to update in array. Approximating.
-[eva] memcpy.c:126: starting to merge loop iterations
-[eva] memcpy.c:131: Call to builtin memcpy
-[eva:alarm] memcpy.c:131: Warning:
+[eva] memcpy.c:126: function memcpy: precondition 'valid_src' got status valid.
+[eva] memcpy.c:126: function memcpy: precondition 'separation' got status valid.
+[kernel] memcpy.c:126: too many locations to update in array. Approximating.
+[eva] memcpy.c:130: starting to merge loop iterations
+[eva] memcpy.c:135: Call to builtin memcpy
+[eva:alarm] memcpy.c:135: Warning:
function memcpy: precondition 'valid_dest' got status unknown.
-[eva] memcpy.c:131: function memcpy: precondition 'valid_src' got status valid.
-[eva] memcpy.c:131: function memcpy: precondition 'separation' got status valid.
-[kernel] memcpy.c:131: too many locations to update in array. Approximating.
-[eva] memcpy.c:135: starting to merge loop iterations
-[eva] memcpy.c:140: Call to builtin memcpy
-[eva:alarm] memcpy.c:140: Warning:
+[eva] memcpy.c:135: function memcpy: precondition 'valid_src' got status valid.
+[eva] memcpy.c:135: function memcpy: precondition 'separation' got status valid.
+[kernel] memcpy.c:135: too many locations to update in array. Approximating.
+[eva] memcpy.c:139: starting to merge loop iterations
+[eva] memcpy.c:144: Call to builtin memcpy
+[eva:alarm] memcpy.c:144: Warning:
function memcpy: precondition 'valid_dest' got status unknown.
-[eva] memcpy.c:140: function memcpy: precondition 'valid_src' got status valid.
-[eva] memcpy.c:140: function memcpy: precondition 'separation' got status valid.
-[kernel] memcpy.c:140: too many locations to update in array. Approximating.
-[eva] memcpy.c:145: Call to builtin memcpy
-[eva:alarm] memcpy.c:145: Warning:
+[eva] memcpy.c:144: function memcpy: precondition 'valid_src' got status valid.
+[eva] memcpy.c:144: function memcpy: precondition 'separation' got status valid.
+[kernel] memcpy.c:144: too many locations to update in array. Approximating.
+[eva] memcpy.c:149: Call to builtin memcpy
+[eva:alarm] memcpy.c:149: Warning:
function memcpy: precondition 'valid_dest' got status unknown.
-[eva:alarm] memcpy.c:145: Warning:
+[eva:alarm] memcpy.c:149: Warning:
function memcpy: precondition 'valid_src' got status unknown.
-[eva] memcpy.c:145: function memcpy: precondition 'separation' got status valid.
-[eva:imprecision] memcpy.c:145:
+[eva] memcpy.c:149: function memcpy: precondition 'separation' got status valid.
+[eva:imprecision] memcpy.c:149:
In memcpy builtin: too many sizes to enumerate, possible loss of precision
-[eva:alarm] memcpy.c:150: Warning: assertion got status unknown.
-[eva] memcpy.c:151: Call to builtin memcpy
-[eva:alarm] memcpy.c:151: Warning:
+[eva:alarm] memcpy.c:154: Warning: assertion got status unknown.
+[eva] memcpy.c:155: Call to builtin memcpy
+[eva:alarm] memcpy.c:155: Warning:
function memcpy: precondition 'valid_dest' got status unknown.
-[eva:alarm] memcpy.c:151: Warning:
+[eva:alarm] memcpy.c:155: Warning:
function memcpy: precondition 'valid_src' got status unknown.
-[eva] memcpy.c:151: function memcpy: precondition 'separation' got status valid.
-[eva:imprecision] memcpy.c:151:
+[eva] memcpy.c:155: function memcpy: precondition 'separation' got status valid.
+[eva:imprecision] memcpy.c:155:
In memcpy builtin: too many sizes to enumerate, possible loss of precision
-[eva:alarm] memcpy.c:152: Warning: assertion got status unknown.
-[eva] memcpy.c:153: Call to builtin memcpy
-[eva] memcpy.c:153: function memcpy: precondition 'valid_dest' got status valid.
-[eva] memcpy.c:153: function memcpy: precondition 'valid_src' got status valid.
-[eva] memcpy.c:153: function memcpy: precondition 'separation' got status valid.
-[eva] Recording results for main
-[from] Computing for function main
-[from] Done for function main
-[eva] Done for function main
-[eva] computing for function main_uninit <- main_all.
- Called from memcpy.c:227.
-[eva] memcpy.c:172: Call to builtin memcpy
-[eva] memcpy.c:172: function memcpy: precondition 'valid_dest' got status valid.
-[eva] memcpy.c:172: function memcpy: precondition 'valid_src' got status valid.
-[eva] memcpy.c:172: function memcpy: precondition 'separation' got status valid.
-[eva:imprecision] memcpy.c:172:
+[eva:alarm] memcpy.c:156: Warning: assertion got status unknown.
+[eva] memcpy.c:157: Call to builtin memcpy
+[eva] memcpy.c:157: function memcpy: precondition 'valid_dest' got status valid.
+[eva] memcpy.c:157: function memcpy: precondition 'valid_src' got status valid.
+[eva] memcpy.c:157: function memcpy: precondition 'separation' got status valid.
+[eva] Recording results for test
+[from] Computing for function test
+[from] Done for function test
+[eva] Done for function test
+[eva] computing for function test_uninit <- main.
+ Called from memcpy.c:228.
+[eva] memcpy.c:176: Call to builtin memcpy
+[eva] memcpy.c:176: function memcpy: precondition 'valid_dest' got status valid.
+[eva] memcpy.c:176: function memcpy: precondition 'valid_src' got status valid.
+[eva] memcpy.c:176: function memcpy: precondition 'separation' got status valid.
+[eva:imprecision] memcpy.c:176:
In memcpy builtin: precise copy of indeterminate values.
-[eva] memcpy.c:173: assertion got status valid.
-[eva] computing for function itv <- main_uninit <- main_all.
- Called from memcpy.c:174.
+[eva] memcpy.c:177: assertion got status valid.
+[eva] computing for function itv <- test_uninit <- main.
+ Called from memcpy.c:178.
[eva] using specification for function itv
[eva] Done for function itv
-[eva] memcpy.c:174: Call to builtin memcpy
-[eva] memcpy.c:174: function memcpy: precondition 'valid_dest' got status valid.
-[eva] memcpy.c:174: function memcpy: precondition 'valid_src' got status valid.
-[eva] memcpy.c:174: function memcpy: precondition 'separation' got status valid.
-[eva:imprecision] memcpy.c:174:
+[eva] memcpy.c:178: Call to builtin memcpy
+[eva] memcpy.c:178: function memcpy: precondition 'valid_dest' got status valid.
+[eva] memcpy.c:178: function memcpy: precondition 'valid_src' got status valid.
+[eva] memcpy.c:178: function memcpy: precondition 'separation' got status valid.
+[eva:imprecision] memcpy.c:178:
In memcpy builtin: too many sizes to enumerate, possible loss of precision
-[eva:imprecision] memcpy.c:174:
+[eva:imprecision] memcpy.c:178:
In memcpy builtin: imprecise copy of indeterminate values.
-[eva] memcpy.c:175: assertion got status valid.
-[eva] computing for function make_unknown <- main_uninit <- main_all.
- Called from memcpy.c:178.
+[eva] memcpy.c:179: assertion got status valid.
+[eva] computing for function make_unknown <- test_uninit <- main.
+ Called from memcpy.c:182.
[eva] using specification for function make_unknown
-[eva] memcpy.c:178: function make_unknown: precondition got status valid.
+[eva] memcpy.c:182: function make_unknown: precondition got status valid.
[eva] Done for function make_unknown
-[eva] memcpy.c:179: Call to builtin memcpy
-[eva] memcpy.c:179: function memcpy: precondition 'valid_dest' got status valid.
-[eva] memcpy.c:179: function memcpy: precondition 'valid_src' got status valid.
-[eva] memcpy.c:179: function memcpy: precondition 'separation' got status valid.
-[eva] memcpy.c:180: assertion got status valid.
-[eva] computing for function itv <- main_uninit <- main_all.
- Called from memcpy.c:181.
+[eva] memcpy.c:183: Call to builtin memcpy
+[eva] memcpy.c:183: function memcpy: precondition 'valid_dest' got status valid.
+[eva] memcpy.c:183: function memcpy: precondition 'valid_src' got status valid.
+[eva] memcpy.c:183: function memcpy: precondition 'separation' got status valid.
+[eva] memcpy.c:184: assertion got status valid.
+[eva] computing for function itv <- test_uninit <- main.
+ Called from memcpy.c:185.
[eva] Done for function itv
-[eva] memcpy.c:181: Call to builtin memcpy
-[eva] memcpy.c:181: function memcpy: precondition 'valid_dest' got status valid.
-[eva] memcpy.c:181: function memcpy: precondition 'valid_src' got status valid.
-[eva] memcpy.c:181: function memcpy: precondition 'separation' got status valid.
-[eva:imprecision] memcpy.c:181:
+[eva] memcpy.c:185: Call to builtin memcpy
+[eva] memcpy.c:185: function memcpy: precondition 'valid_dest' got status valid.
+[eva] memcpy.c:185: function memcpy: precondition 'valid_src' got status valid.
+[eva] memcpy.c:185: function memcpy: precondition 'separation' got status valid.
+[eva:imprecision] memcpy.c:185:
In memcpy builtin: too many sizes to enumerate, possible loss of precision
-[eva:imprecision] memcpy.c:181:
+[eva:imprecision] memcpy.c:185:
In memcpy builtin: imprecise copy of indeterminate values.
-[eva:alarm] memcpy.c:182: Warning:
+[eva:alarm] memcpy.c:186: Warning:
accessing uninitialized left-value. assert \initialized(&b[11]);
-[eva] computing for function make_unknown <- main_uninit <- main_all.
- Called from memcpy.c:185.
-[eva] memcpy.c:185: function make_unknown: precondition got status valid.
+[eva] computing for function make_unknown <- test_uninit <- main.
+ Called from memcpy.c:189.
+[eva] memcpy.c:189: function make_unknown: precondition got status valid.
[eva] Done for function make_unknown
-[eva] memcpy.c:187: Call to builtin memcpy
-[eva] memcpy.c:187: function memcpy: precondition 'valid_dest' got status valid.
-[eva] memcpy.c:187: function memcpy: precondition 'valid_src' got status valid.
-[eva] memcpy.c:187: function memcpy: precondition 'separation' got status valid.
-[eva:imprecision] memcpy.c:187:
+[eva] memcpy.c:191: Call to builtin memcpy
+[eva] memcpy.c:191: function memcpy: precondition 'valid_dest' got status valid.
+[eva] memcpy.c:191: function memcpy: precondition 'valid_src' got status valid.
+[eva] memcpy.c:191: function memcpy: precondition 'separation' got status valid.
+[eva:imprecision] memcpy.c:191:
In memcpy builtin: precise copy of indeterminate values.
-[eva] memcpy.c:188: assertion got status valid.
-[eva] computing for function itv <- main_uninit <- main_all.
- Called from memcpy.c:190.
+[eva] memcpy.c:192: assertion got status valid.
+[eva] computing for function itv <- test_uninit <- main.
+ Called from memcpy.c:194.
[eva] Done for function itv
-[eva] memcpy.c:190: Call to builtin memcpy
-[eva] memcpy.c:190: function memcpy: precondition 'valid_dest' got status valid.
-[eva] memcpy.c:190: function memcpy: precondition 'valid_src' got status valid.
-[eva] memcpy.c:190: function memcpy: precondition 'separation' got status valid.
-[eva:imprecision] memcpy.c:190:
+[eva] memcpy.c:194: Call to builtin memcpy
+[eva] memcpy.c:194: function memcpy: precondition 'valid_dest' got status valid.
+[eva] memcpy.c:194: function memcpy: precondition 'valid_src' got status valid.
+[eva] memcpy.c:194: function memcpy: precondition 'separation' got status valid.
+[eva:imprecision] memcpy.c:194:
In memcpy builtin: too many sizes to enumerate, possible loss of precision
-[eva:imprecision] memcpy.c:190:
+[eva:imprecision] memcpy.c:194:
In memcpy builtin: imprecise copy of indeterminate values.
-[eva] memcpy.c:191: assertion got status valid.
-[eva:alarm] memcpy.c:192: Warning:
+[eva] memcpy.c:195: assertion got status valid.
+[eva:alarm] memcpy.c:196: Warning:
accessing uninitialized left-value. assert \initialized(&b[8]);
-[eva] computing for function make_unknown <- main_uninit <- main_all.
- Called from memcpy.c:196.
-[eva] memcpy.c:196: function make_unknown: precondition got status valid.
+[eva] computing for function make_unknown <- test_uninit <- main.
+ Called from memcpy.c:200.
+[eva] memcpy.c:200: function make_unknown: precondition got status valid.
[eva] Done for function make_unknown
-[eva] computing for function make_unknown <- main_uninit <- main_all.
- Called from memcpy.c:197.
-[eva] memcpy.c:197: function make_unknown: precondition got status valid.
+[eva] computing for function make_unknown <- test_uninit <- main.
+ Called from memcpy.c:201.
+[eva] memcpy.c:201: function make_unknown: precondition got status valid.
[eva] Done for function make_unknown
-[eva] memcpy.c:198: Call to builtin memcpy
-[eva] memcpy.c:198: function memcpy: precondition 'valid_dest' got status valid.
-[eva] memcpy.c:198: function memcpy: precondition 'valid_src' got status valid.
-[eva] memcpy.c:198: function memcpy: precondition 'separation' got status valid.
-[eva] memcpy.c:199: assertion got status valid.
-[eva] computing for function itv <- main_uninit <- main_all.
- Called from memcpy.c:200.
+[eva] memcpy.c:202: Call to builtin memcpy
+[eva] memcpy.c:202: function memcpy: precondition 'valid_dest' got status valid.
+[eva] memcpy.c:202: function memcpy: precondition 'valid_src' got status valid.
+[eva] memcpy.c:202: function memcpy: precondition 'separation' got status valid.
+[eva] memcpy.c:203: assertion got status valid.
+[eva] computing for function itv <- test_uninit <- main.
+ Called from memcpy.c:204.
[eva] Done for function itv
-[eva] memcpy.c:200: Call to builtin memcpy
-[eva] memcpy.c:200: function memcpy: precondition 'valid_dest' got status valid.
-[eva] memcpy.c:200: function memcpy: precondition 'valid_src' got status valid.
-[eva] memcpy.c:200: function memcpy: precondition 'separation' got status valid.
-[eva:imprecision] memcpy.c:200:
+[eva] memcpy.c:204: Call to builtin memcpy
+[eva] memcpy.c:204: function memcpy: precondition 'valid_dest' got status valid.
+[eva] memcpy.c:204: function memcpy: precondition 'valid_src' got status valid.
+[eva] memcpy.c:204: function memcpy: precondition 'separation' got status valid.
+[eva:imprecision] memcpy.c:204:
In memcpy builtin: too many sizes to enumerate, possible loss of precision
-[eva:imprecision] memcpy.c:200:
+[eva:imprecision] memcpy.c:204:
In memcpy builtin: imprecise copy of indeterminate values.
-[eva:alarm] memcpy.c:201: Warning:
+[eva:alarm] memcpy.c:205: Warning:
accessing uninitialized left-value. assert \initialized(&b[11]);
-[eva] Recording results for main_uninit
-[from] Computing for function main_uninit
-[from] Done for function main_uninit
-[eva] Done for function main_uninit
-[eva] computing for function main_local <- main_all.
- Called from memcpy.c:228.
-[eva] memcpy.c:209: Call to builtin memcpy
-[eva] memcpy.c:209: function memcpy: precondition 'valid_dest' got status valid.
-[eva] memcpy.c:209: function memcpy: precondition 'valid_src' got status valid.
-[eva] memcpy.c:209: function memcpy: precondition 'separation' got status valid.
-[eva:locals-escaping] memcpy.c:210: Warning:
- locals {y} escaping the scope of a block of main_local through p
-[eva] memcpy.c:212:
+[eva] Recording results for test_uninit
+[from] Computing for function test_uninit
+[from] Done for function test_uninit
+[eva] Done for function test_uninit
+[eva] computing for function test_local <- main.
+ Called from memcpy.c:229.
+[eva] memcpy.c:213: Call to builtin memcpy
+[eva] memcpy.c:213: function memcpy: precondition 'valid_dest' got status valid.
+[eva] memcpy.c:213: function memcpy: precondition 'valid_src' got status valid.
+[eva] memcpy.c:213: function memcpy: precondition 'separation' got status valid.
+[eva:locals-escaping] memcpy.c:214: Warning:
+ locals {y} escaping the scope of a block of test_local through p
+[eva] memcpy.c:216:
Frama_C_dump_each:
# cvalue:
- NULL[rbits 800000 to 800015] ∈ [--..--]
__fc_heap_status ∈ [--..--]
__fc_strtok_ptr ∈ {0}
__fc_strerror[0..63] ∈ [--..--]
@@ -347,33 +345,30 @@
p ∈ ESCAPINGADDR
q ∈ {0}
==END OF DUMP==
-[eva] Recording results for main_local
-[from] Computing for function main_local
-[from] Done for function main_local
-[eva] Done for function main_local
-[eva] computing for function copy_0 <- main_all.
- Called from memcpy.c:229.
-[eva] memcpy.c:220: Call to builtin memcpy
-[eva:alarm] memcpy.c:220: Warning:
- function memcpy: precondition 'valid_dest' got status invalid.
-[eva] memcpy.c:220:
- function memcpy: no state left, precondition 'valid_src' got status valid.
-[eva] memcpy.c:220:
- function memcpy: no state left, precondition 'separation' got status valid.
+[eva] Recording results for test_local
+[from] Computing for function test_local
+[from] Done for function test_local
+[eva] Done for function test_local
+[eva] computing for function copy_0 <- main.
+ Called from memcpy.c:230.
[eva] memcpy.c:221: Call to builtin memcpy
-[eva] memcpy.c:221: function memcpy: precondition 'valid_dest' got status valid.
[eva:alarm] memcpy.c:221: Warning:
- function memcpy: precondition 'valid_src' got status invalid.
-[eva] memcpy.c:221:
- function memcpy: no state left, precondition 'separation' got status valid.
+ function memcpy: precondition 'valid_dest' got status unknown.
+[eva] memcpy.c:221: function memcpy: precondition 'valid_src' got status valid.
+[eva] memcpy.c:221: function memcpy: precondition 'separation' got status valid.
+[eva] memcpy.c:222: Call to builtin memcpy
+[eva] memcpy.c:222: function memcpy: precondition 'valid_dest' got status valid.
+[eva:alarm] memcpy.c:222: Warning:
+ function memcpy: precondition 'valid_src' got status unknown.
+[eva] memcpy.c:222: function memcpy: precondition 'separation' got status valid.
[eva] Recording results for copy_0
[from] Computing for function copy_0
[from] Done for function copy_0
[eva] Done for function copy_0
-[eva] Recording results for main_all
-[from] Computing for function main_all
-[from] Done for function main_all
-[eva] Done for function main_all
+[eva] Recording results for main
+[from] Computing for function main
+[from] Done for function main
+[eva] Done for function main
[scope:rm_asserts] removing 1 assertion(s)
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function init:
@@ -408,15 +403,6 @@
p ∈ {{ &c ; "abc" }}
[eva:final-states] Values at end of function copy_0:
-[eva:final-states] Values at end of function main_local:
- p ∈ ESCAPINGADDR
- q ∈ {0}
-[eva:final-states] Values at end of function main_uninit:
- a[0..9] ∈ [--..--] or UNINITIALIZED
- [10..49] ∈ UNINITIALIZED
- b[0..24] ∈ [--..--] or UNINITIALIZED
- [25..49] ∈ UNINITIALIZED
- r ∈ [0..255]
[eva:final-states] Values at end of function many:
tm[0..999] ∈ {0; 1684234849}
um{[0..998]#; [999][bits 0 to 15]} ∈ {0; 25185} repeated %16
@@ -435,7 +421,7 @@
ty.ts ∈ {1}
.[bits 16 to 31] ∈ {0}
.ti ∈ {2}
-[eva:final-states] Values at end of function main:
+[eva:final-states] Values at end of function test:
src[0] ∈ {1}
[1] ∈ {2}
[2] ∈ {3}
@@ -572,7 +558,7 @@
v2.x ∈ {5}
.y ∈ {7}
{.p; .padding[0..23]} ∈ {0}
- v3 ∈ {{ garbled mix of &{v1} (origin: Misaligned read {memcpy.c:87}) }}
+ v3 ∈ {{ garbled mix of &{v1} (origin: Misaligned read {memcpy.c:91}) }}
v4.x[bits 0 to 7]# ∈ {0; 5}%32, bits 0 to 7
.x[bits 8 to 31] ∈ [--..--]
.y ∈ {{ (int)&t }}
@@ -583,7 +569,7 @@
.x[bits 8 to 31] ∈ [--..--]
.y[bits 0 to 7]# ∈ {{ NULL + [--..--] ; (? *)&t }}%32, bits 0 to 7
{.y[bits 8 to 31]; .p; .padding[0..14]} ∈
- {{ garbled mix of &{t} (origin: Merge {memcpy.c:91}) }}
+ {{ garbled mix of &{t} (origin: Merge {memcpy.c:95}) }}
.padding[15]# ∈ {{ NULL + [--..--] ; (? *)&t }}%32, bits 24 to 31
.padding[16..23] ∈ [--..--]
t{[0]; [1]{.x; .y}} ∈ {0}
@@ -617,153 +603,162 @@
[5] ∈ {6} or UNINITIALIZED
[6..149] ∈ UNINITIALIZED
maybesize ∈ {0; 1; 2; 3; 4; 5; 6}
-[eva:final-states] Values at end of function main_all:
+[eva:final-states] Values at end of function test_local:
+ p ∈ ESCAPINGADDR
+ q ∈ {0}
+[eva:final-states] Values at end of function test_uninit:
+ a[0..9] ∈ [--..--] or UNINITIALIZED
+ [10..49] ∈ UNINITIALIZED
+ b[0..24] ∈ [--..--] or UNINITIALIZED
+ [25..49] ∈ UNINITIALIZED
+ r ∈ [0..255]
+[eva:final-states] Values at end of function main:
NON TERMINATING FUNCTION
[from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
-[from] call to memcpy at memcpy.c:28 (by buggy):
+[from] call to memcpy at memcpy.c:32 (by buggy):
c FROM "d"[bits 0 to 7]
\result FROM dest
-[from] call to memcpy at memcpy.c:220 (by copy_0):
- \result FROM dest
[from] call to memcpy at memcpy.c:221 (by copy_0):
\result FROM dest
-[from] call to memcpy at memcpy.c:209 (by main_local):
- p FROM q
- \result FROM dest
-[from] call to Frama_C_dump_each at memcpy.c:212 (by main_local):
- \result FROM \nothing
-[from] call to memcpy at memcpy.c:172 (by main_uninit):
- b[0..9] FROM a[0..9]
- \result FROM dest
-[from] call to memcpy at memcpy.c:174 (by main_uninit):
- b[0..24] FROM a[0..24] (and SELF)
- \result FROM dest
-[from] call to itv at memcpy.c:174 (by main_uninit):
- \result FROM l; u
-[from] call to make_unknown at memcpy.c:178 (by main_uninit):
- a[0..9] FROM maybe
-[from] call to memcpy at memcpy.c:179 (by main_uninit):
- b[0..9] FROM a[0..9]
- \result FROM dest
-[from] call to memcpy at memcpy.c:181 (by main_uninit):
- b[0..24] FROM a[0..24] (and SELF)
- \result FROM dest
-[from] call to itv at memcpy.c:181 (by main_uninit):
- \result FROM l; u
-[from] call to make_unknown at memcpy.c:185 (by main_uninit):
- b[0..9] FROM maybe
-[from] call to memcpy at memcpy.c:187 (by main_uninit):
- b[0..9] FROM a[0..9]
- \result FROM dest
-[from] call to memcpy at memcpy.c:190 (by main_uninit):
- b[0..24] FROM a[0..24] (and SELF)
- \result FROM dest
-[from] call to itv at memcpy.c:190 (by main_uninit):
- \result FROM l; u
-[from] call to make_unknown at memcpy.c:196 (by main_uninit):
- a[0..9] FROM maybe
-[from] call to make_unknown at memcpy.c:197 (by main_uninit):
- b[0..9] FROM maybe
-[from] call to memcpy at memcpy.c:198 (by main_uninit):
- b[0..9] FROM a[0..9]
- \result FROM dest
-[from] call to memcpy at memcpy.c:200 (by main_uninit):
- b[0..24] FROM a[0..24] (and SELF)
+[from] call to memcpy at memcpy.c:222 (by copy_0):
\result FROM dest
-[from] call to itv at memcpy.c:200 (by main_uninit):
- \result FROM l; u
-[from] call to memcpy at memcpy.c:47 (by many):
+[from] call to memcpy at memcpy.c:51 (by many):
tm[0..999] FROM s[0..3] (and SELF)
\result FROM dest
-[from] call to memcpy at memcpy.c:49 (by many):
+[from] call to memcpy at memcpy.c:53 (by many):
um{[0..998]; [999][bits 0 to 15]} FROM s[0..1] (and SELF)
\result FROM dest
-[from] call to memcpy at memcpy.c:53 (by many):
+[from] call to memcpy at memcpy.c:57 (by many):
ttyp[0..999] FROM ty (and SELF)
\result FROM dest
-[from] call to buggy at memcpy.c:61 (by main):
+[from] call to buggy at memcpy.c:65 (by test):
NO EFFECTS
-[from] call to many at memcpy.c:63 (by main):
+[from] call to many at memcpy.c:67 (by test):
tm[0] FROM \nothing
[1..999] FROM \nothing (and SELF)
um[0] FROM \nothing
{[1..998]; [999][bits 0 to 15]} FROM \nothing (and SELF)
ttyp[0] FROM \nothing
[1..999] FROM \nothing (and SELF)
-[from] call to init at memcpy.c:65 (by main):
+[from] call to init at memcpy.c:69 (by test):
src[0..19] FROM \nothing (and SELF)
dst1[0..19] FROM \nothing (and SELF)
dst2[0..19] FROM \nothing (and SELF)
dst3[0..19] FROM \nothing (and SELF)
dst4[0..19] FROM \nothing (and SELF)
dst5[0..99] FROM \nothing (and SELF)
-[from] call to memcpy at memcpy.c:68 (by main):
+[from] call to memcpy at memcpy.c:72 (by test):
dst1[1..5] FROM src[2..6]
[6..15] FROM src[7..16] (and SELF)
\result FROM dest
-[from] call to memcpy at memcpy.c:70 (by main):
+[from] call to memcpy at memcpy.c:74 (by test):
dst2[1..10] FROM src[2..11]
[11..19] FROM src[12..19] (and SELF)
\result FROM dest
-[from] call to memcpy at memcpy.c:73 (by main):
+[from] call to memcpy at memcpy.c:77 (by test):
dst3[5..9] FROM src[2..6]
[10..18] FROM src[7..15] (and SELF)
\result FROM dest
-[from] call to memcpy at memcpy.c:75 (by main):
+[from] call to memcpy at memcpy.c:79 (by test):
dst4[5..14] FROM src[2..11]
[15..19] FROM src[12..19] (and SELF)
\result FROM dest
-[from] call to memcpy at memcpy.c:83 (by main):
+[from] call to memcpy at memcpy.c:87 (by test):
v2 FROM v1
\result FROM dest
-[from] call to memcpy at memcpy.c:85 (by main):
+[from] call to memcpy at memcpy.c:89 (by test):
t[2] FROM t[0]
[3] FROM t[1] (and SELF)
\result FROM dest
-[from] call to memcpy at memcpy.c:87 (by main):
+[from] call to memcpy at memcpy.c:91 (by test):
v3 FROM t[0..3]
\result FROM dest
-[from] call to memcpy at memcpy.c:89 (by main):
+[from] call to memcpy at memcpy.c:93 (by test):
v4 FROM v1{.x; .y; .p; .padding[0..3]} (and SELF)
\result FROM dest
-[from] call to memcpy at memcpy.c:91 (by main):
+[from] call to memcpy at memcpy.c:95 (by test):
v5 FROM v4{.x; .y; .p; .padding[0..3]} (and SELF)
\result FROM dest
-[from] call to memcpy at memcpy.c:96 (by main):
+[from] call to memcpy at memcpy.c:100 (by test):
x FROM x (and SELF)
\result FROM dest
-[from] call to memcpy at memcpy.c:101 (by main):
+[from] call to memcpy at memcpy.c:105 (by test):
dst5[0..4] FROM src[0..4] (and SELF)
{[5..19]; [25..33]} FROM src[5..13] (and SELF)
[20..24] FROM src[0..13] (and SELF)
\result FROM dest
-[from] call to memcpy at memcpy.c:105 (by main):
+[from] call to memcpy at memcpy.c:109 (by test):
dst5[40] FROM src[0] (and SELF)
{[41..69]; [71..88]} FROM src[1..18] (and SELF)
[70] FROM src[0..18] (and SELF)
\result FROM dest
-[from] call to memcpy at memcpy.c:114 (by main):
+[from] call to memcpy at memcpy.c:118 (by test):
ptop1[4..799] FROM src[0..3] (and SELF)
\result FROM dest
-[from] call to memcpy at memcpy.c:122 (by main):
+[from] call to memcpy at memcpy.c:126 (by test):
ptop2[2..749] FROM src[1..4] (and SELF)
\result FROM dest
-[from] call to memcpy at memcpy.c:131 (by main):
+[from] call to memcpy at memcpy.c:135 (by test):
ptop3[2..797] FROM src[2..5] (and SELF)
\result FROM dest
-[from] call to memcpy at memcpy.c:140 (by main):
+[from] call to memcpy at memcpy.c:144 (by test):
ptop4[2..798] FROM src[2..6] (and SELF)
\result FROM dest
-[from] call to memcpy at memcpy.c:145 (by main):
+[from] call to memcpy at memcpy.c:149 (by test):
garbledsize[10..99] FROM src[0..19] (and SELF)
\result FROM dest
-[from] call to memcpy at memcpy.c:151 (by main):
+[from] call to memcpy at memcpy.c:155 (by test):
dstmaybesize1[0..14] FROM src[0..19] (and SELF)
\result FROM dest
-[from] call to memcpy at memcpy.c:153 (by main):
+[from] call to memcpy at memcpy.c:157 (by test):
dstmaybesize2[0..5] FROM src[0..5] (and SELF)
\result FROM dest
-[from] call to main at memcpy.c:226 (by main_all):
+[from] call to memcpy at memcpy.c:213 (by test_local):
+ p FROM q
+ \result FROM dest
+[from] call to Frama_C_dump_each at memcpy.c:216 (by test_local):
+ \result FROM \nothing
+[from] call to memcpy at memcpy.c:176 (by test_uninit):
+ b[0..9] FROM a[0..9]
+ \result FROM dest
+[from] call to memcpy at memcpy.c:178 (by test_uninit):
+ b[0..24] FROM a[0..24] (and SELF)
+ \result FROM dest
+[from] call to itv at memcpy.c:178 (by test_uninit):
+ \result FROM l; u
+[from] call to make_unknown at memcpy.c:182 (by test_uninit):
+ a[0..9] FROM maybe
+[from] call to memcpy at memcpy.c:183 (by test_uninit):
+ b[0..9] FROM a[0..9]
+ \result FROM dest
+[from] call to memcpy at memcpy.c:185 (by test_uninit):
+ b[0..24] FROM a[0..24] (and SELF)
+ \result FROM dest
+[from] call to itv at memcpy.c:185 (by test_uninit):
+ \result FROM l; u
+[from] call to make_unknown at memcpy.c:189 (by test_uninit):
+ b[0..9] FROM maybe
+[from] call to memcpy at memcpy.c:191 (by test_uninit):
+ b[0..9] FROM a[0..9]
+ \result FROM dest
+[from] call to memcpy at memcpy.c:194 (by test_uninit):
+ b[0..24] FROM a[0..24] (and SELF)
+ \result FROM dest
+[from] call to itv at memcpy.c:194 (by test_uninit):
+ \result FROM l; u
+[from] call to make_unknown at memcpy.c:200 (by test_uninit):
+ a[0..9] FROM maybe
+[from] call to make_unknown at memcpy.c:201 (by test_uninit):
+ b[0..9] FROM maybe
+[from] call to memcpy at memcpy.c:202 (by test_uninit):
+ b[0..9] FROM a[0..9]
+ \result FROM dest
+[from] call to memcpy at memcpy.c:204 (by test_uninit):
+ b[0..24] FROM a[0..24] (and SELF)
+ \result FROM dest
+[from] call to itv at memcpy.c:204 (by test_uninit):
+ \result FROM l; u
+[from] call to test at memcpy.c:227 (by main):
src[0..19] FROM \nothing (and SELF)
dst1{[0]; [16..19]} FROM \nothing (and SELF)
[1..5] FROM src[2..6]
@@ -799,11 +794,11 @@
t[1] FROM v2
[2] FROM t[0]
[3] FROM v2 (and SELF)
-[from] call to main_uninit at memcpy.c:227 (by main_all):
+[from] call to test_uninit at memcpy.c:228 (by main):
NO EFFECTS
-[from] call to main_local at memcpy.c:228 (by main_all):
+[from] call to test_local at memcpy.c:229 (by main):
NO EFFECTS
-[from] call to copy_0 at memcpy.c:229 (by main_all):
+[from] call to copy_0 at memcpy.c:230 (by main):
NO EFFECTS
[from] entry point:
NON TERMINATING - NO EFFECTS
@@ -842,28 +837,6 @@
i
Sure outputs:
\nothing
-[inout] Out (internal) for function main_local:
- p; q
-[inout] Inputs for function main_local:
- \nothing
-[inout] InOut (internal) for function main_local:
- Operational inputs:
- \nothing
- Operational inputs on termination:
- \nothing
- Sure outputs:
- p; q
-[inout] Out (internal) for function main_uninit:
- a[0..9]; b[0..24]; r; tmp; tmp_0; tmp_1; tmp_2
-[inout] Inputs for function main_uninit:
- maybe
-[inout] InOut (internal) for function main_uninit:
- Operational inputs:
- maybe; a[0..24]; b[11]
- Operational inputs on termination:
- maybe; a[0..24]; b[11]
- Sure outputs:
- r
[inout] Out (internal) for function many:
tm[0..999]; um{[0..998]; [999][bits 0 to 15]}; ttyp[0..999]; s[0..4];
p; ty{.ts; .ti}
@@ -876,16 +849,16 @@
maybe; ty.[bits 16 to 31]
Sure outputs:
tm[0]; um[0]; ttyp[0]; s[0..4]; p; ty{.ts; .ti}
-[inout] Out (internal) for function main:
+[inout] Out (internal) for function test:
src[0..19]; dst1[0..19]; dst2[0..19]; dst3[0..19]; dst4[0..19];
dst5[0..99]; tm[0..999]; um{[0..998]; [999][bits 0 to 15]}; ttyp[0..999];
v1{.x; .y}; v2; v3; v4; v5; t[1..3]; b; x; p; ptop1[4..799]; pptop;
ptop2[2..749]; ptop3[2..797]; ptop4[2..798]; garbledsize[10..99];
pgarbledsize; dstmaybesize1[0..14]; dstmaybesize2[0..5]; maybesize
-[inout] Inputs for function main:
- NULL[100000..100001]; i; src[0..19]; maybe; v1; v2;
- v4{.x; .y; .p; .padding[0..3]}; t[0..3]; "d"[bits 0 to 7]
-[inout] InOut (internal) for function main:
+[inout] Inputs for function test:
+ i; src[0..19]; maybe; v1; v2; v4{.x; .y; .p; .padding[0..3]}; t[0..3];
+ "d"[bits 0 to 7]
+[inout] InOut (internal) for function test:
Operational inputs:
i; src[0..19]; maybe; v1{.p; .padding[0..23]}; v2;
v4{.x; {.p; .padding[0..3]}}; t{[0]; [3]}; a; b; "d"[bits 0 to 7]
@@ -895,14 +868,36 @@
Sure outputs:
dst1[1..5]; dst2[1..10]; dst3[5..9]; dst4[5..14]; tm[0]; um[0]; ttyp[0];
v1{.x; .y}; v2; v3; v4.y; t[1..2]; b; p; pptop; pgarbledsize; maybesize
-[inout] Out (internal) for function main_all:
+[inout] Out (internal) for function test_local:
+ p; q
+[inout] Inputs for function test_local:
+ \nothing
+[inout] InOut (internal) for function test_local:
+ Operational inputs:
+ \nothing
+ Operational inputs on termination:
+ \nothing
+ Sure outputs:
+ p; q
+[inout] Out (internal) for function test_uninit:
+ a[0..9]; b[0..24]; r; tmp; tmp_0; tmp_1; tmp_2
+[inout] Inputs for function test_uninit:
+ maybe
+[inout] InOut (internal) for function test_uninit:
+ Operational inputs:
+ maybe; a[0..24]; b[11]
+ Operational inputs on termination:
+ maybe; a[0..24]; b[11]
+ Sure outputs:
+ r
+[inout] Out (internal) for function main:
src[0..19]; dst1[0..19]; dst2[0..19]; dst3[0..19]; dst4[0..19];
dst5[0..99]; tm[0..999]; um{[0..998]; [999][bits 0 to 15]}; ttyp[0..999];
v1{.x; .y}; v2; v3; v4; v5; t[1..3]
-[inout] Inputs for function main_all:
- NULL[100000..100001]; i; src[0..19]; maybe; v1; v2;
- v4{.x; .y; .p; .padding[0..3]}; t[0..3]; "d"[bits 0 to 7]
-[inout] InOut (internal) for function main_all:
+[inout] Inputs for function main:
+ i; src[0..19]; maybe; v1; v2; v4{.x; .y; .p; .padding[0..3]}; t[0..3];
+ "d"[bits 0 to 7]
+[inout] InOut (internal) for function main:
Operational inputs:
i; src[0..19]; maybe; v1{.p; .padding[0..23]}; v2;
v4{.x; {.p; .padding[0..3]}}; t{[0]; [3]}; "d"[bits 0 to 7]
@@ -1075,48 +1070,10 @@
--- Properties of Function 'memcpy'
--------------------------------------------------------------------------------
-[ Alarm ] Pre-condition 'valid_dest'
- By Call Preconditions, with pending:
- - Unreachable call 'memcpy' (file memcpy.c, line 220)
- - Instance of 'Pre-condition 'valid_dest'' of 'buggy' at call 'memcpy' (file memcpy.c, line 28)
-
- - Instance of 'Pre-condition 'valid_dest'' of 'main' at call 'memcpy' (file memcpy.c, line 70)
-
- - Instance of 'Pre-condition 'valid_dest'' of 'main' at call 'memcpy' (file memcpy.c, line 75)
-
- - Instance of 'Pre-condition 'valid_dest'' of 'main' at call 'memcpy' (file memcpy.c, line 89)
-
- - Instance of 'Pre-condition 'valid_dest'' of 'main' at call 'memcpy' (file memcpy.c, line 91)
-
- - Instance of 'Pre-condition 'valid_dest'' of 'main' at call 'memcpy' (file memcpy.c, line 96)
-
- - Instance of 'Pre-condition 'valid_dest'' of 'main' at call 'memcpy' (file memcpy.c, line 114)
-
- - Instance of 'Pre-condition 'valid_dest'' of 'main' at call 'memcpy' (file memcpy.c, line 122)
-
- - Instance of 'Pre-condition 'valid_dest'' of 'main' at call 'memcpy' (file memcpy.c, line 131)
-
- - Instance of 'Pre-condition 'valid_dest'' of 'main' at call 'memcpy' (file memcpy.c, line 140)
-
- - Instance of 'Pre-condition 'valid_dest'' of 'main' at call 'memcpy' (file memcpy.c, line 145)
-
- - Instance of 'Pre-condition 'valid_dest'' of 'main' at call 'memcpy' (file memcpy.c, line 151)
-
-[ Alarm ] Pre-condition 'valid_src'
- By Call Preconditions, with pending:
- - Unreachable call 'memcpy' (file memcpy.c, line 221)
- - Instance of 'Pre-condition 'valid_src'' of 'main' at call 'memcpy' (file memcpy.c, line 70)
-
- - Instance of 'Pre-condition 'valid_src'' of 'main' at call 'memcpy' (file memcpy.c, line 75)
-
- - Instance of 'Pre-condition 'valid_src'' of 'main' at call 'memcpy' (file memcpy.c, line 87)
-
- - Instance of 'Pre-condition 'valid_src'' of 'main' at call 'memcpy' (file memcpy.c, line 96)
-
- - Instance of 'Pre-condition 'valid_src'' of 'main' at call 'memcpy' (file memcpy.c, line 145)
-
- - Instance of 'Pre-condition 'valid_src'' of 'main' at call 'memcpy' (file memcpy.c, line 151)
-
+[ - ] Pre-condition 'valid_dest'
+ tried with Call Preconditions.
+[ - ] Pre-condition 'valid_src'
+ tried with Call Preconditions.
[ - ] Pre-condition 'separation'
tried with Call Preconditions.
[ Extern ] Post-condition 'copied_contents'
@@ -1836,13 +1793,13 @@
--- Properties of Function 'buggy'
--------------------------------------------------------------------------------
-[ - ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 28)
+[ - ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 32)
tried with Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 28)
+[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 32)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 28)
+[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 32)
by Eva.
@@ -1850,228 +1807,228 @@
--- Properties of Function 'many'
--------------------------------------------------------------------------------
-[ - ] Assertion (file memcpy.c, line 44)
+[ - ] Assertion (file memcpy.c, line 48)
tried with Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 47)
+[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 51)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 47)
+[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 51)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 47)
+[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 51)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 49)
+[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 53)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 49)
+[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 53)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 49)
+[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 53)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 53)
+[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 57)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 53)
+[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 57)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 53)
+[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 57)
by Eva.
--------------------------------------------------------------------------------
---- Properties of Function 'main'
+--- Properties of Function 'test'
--------------------------------------------------------------------------------
-[ - ] Assertion (file memcpy.c, line 67)
+[ - ] Assertion (file memcpy.c, line 71)
tried with Eva.
-[ - ] Assertion (file memcpy.c, line 72)
+[ - ] Assertion (file memcpy.c, line 76)
tried with Eva.
-[ - ] Assertion (file memcpy.c, line 103)
+[ - ] Assertion (file memcpy.c, line 107)
tried with Eva.
-[ - ] Assertion (file memcpy.c, line 150)
+[ - ] Assertion (file memcpy.c, line 154)
tried with Eva.
-[ - ] Assertion (file memcpy.c, line 152)
+[ - ] Assertion (file memcpy.c, line 156)
tried with Eva.
-[ - ] Assertion 'Eva,pointer_downcast' (file memcpy.c, line 87)
+[ - ] Assertion 'Eva,pointer_downcast' (file memcpy.c, line 91)
tried with Eva.
-[ - ] Assertion 'Eva,pointer_downcast' (file memcpy.c, line 89)
+[ - ] Assertion 'Eva,pointer_downcast' (file memcpy.c, line 93)
tried with Eva.
-[ Partial ] Assertion 'Eva,pointer_downcast' (file memcpy.c, line 90)
+[ Partial ] Assertion 'Eva,pointer_downcast' (file memcpy.c, line 94)
By RedundantAlarms, with pending:
- - Assertion 'Eva,pointer_downcast' (file memcpy.c, line 87)
-[ - ] Assertion 'Eva,pointer_downcast' (file memcpy.c, line 91)
+ - Assertion 'Eva,pointer_downcast' (file memcpy.c, line 91)
+[ - ] Assertion 'Eva,pointer_downcast' (file memcpy.c, line 95)
tried with Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 68)
+[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 72)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 68)
+[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 72)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 68)
+[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 72)
by Eva.
-[ - ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 70)
+[ - ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 74)
tried with Eva.
-[ - ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 70)
+[ - ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 74)
tried with Eva.
-[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 70)
+[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 74)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 73)
+[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 77)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 73)
+[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 77)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 73)
+[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 77)
by Eva.
-[ - ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 75)
+[ - ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 79)
tried with Eva.
-[ - ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 75)
+[ - ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 79)
tried with Eva.
-[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 75)
+[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 79)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 83)
+[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 87)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 83)
+[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 87)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 83)
+[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 87)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 85)
+[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 89)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 85)
+[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 89)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 85)
+[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 89)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 87)
+[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 91)
by Eva.
-[ - ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 87)
+[ - ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 91)
tried with Eva.
-[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 87)
+[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 91)
by Eva.
-[ - ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 89)
+[ - ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 93)
tried with Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 89)
+[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 93)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 89)
+[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 93)
by Eva.
-[ - ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 91)
+[ - ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 95)
tried with Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 91)
+[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 95)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 91)
+[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 95)
by Eva.
-[ - ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 96)
+[ - ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 100)
tried with Eva.
-[ - ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 96)
+[ - ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 100)
tried with Eva.
-[ - ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 96)
+[ - ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 100)
tried with Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 101)
+[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 105)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 101)
+[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 105)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 101)
+[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 105)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 105)
+[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 109)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 105)
+[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 109)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 105)
+[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 109)
by Eva.
-[ - ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 114)
+[ - ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 118)
tried with Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 114)
+[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 118)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 114)
+[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 118)
by Eva.
-[ - ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 122)
+[ - ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 126)
tried with Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 122)
+[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 126)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 122)
+[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 126)
by Eva.
-[ - ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 131)
+[ - ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 135)
tried with Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 131)
+[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 135)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 131)
+[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 135)
by Eva.
-[ - ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 140)
+[ - ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 144)
tried with Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 140)
+[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 144)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 140)
+[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 144)
by Eva.
-[ - ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 145)
+[ - ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 149)
tried with Eva.
-[ - ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 145)
+[ - ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 149)
tried with Eva.
-[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 145)
+[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 149)
by Eva.
-[ - ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 151)
+[ - ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 155)
tried with Eva.
-[ - ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 151)
+[ - ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 155)
tried with Eva.
-[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 151)
+[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 155)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 153)
+[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 157)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 153)
+[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 157)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 153)
+[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 157)
by Eva.
@@ -2079,11 +2036,11 @@
--- Properties of Function 'itv'
--------------------------------------------------------------------------------
-[ Extern ] Post-condition (file memcpy.c, line 158)
+[ Extern ] Post-condition (file memcpy.c, line 162)
Unverifiable but considered Valid.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file memcpy.c, line 157)
+[ Extern ] Froms (file memcpy.c, line 161)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -2092,135 +2049,135 @@
--- Properties of Function 'make_unknown'
--------------------------------------------------------------------------------
-[ Valid ] Pre-condition (file memcpy.c, line 161)
+[ Valid ] Pre-condition (file memcpy.c, line 165)
by Call Preconditions.
-[ Extern ] Post-condition (file memcpy.c, line 163)
+[ Extern ] Post-condition (file memcpy.c, line 167)
Unverifiable but considered Valid.
-[ Extern ] Assigns (file memcpy.c, line 162)
+[ Extern ] Assigns (file memcpy.c, line 166)
Unverifiable but considered Valid.
-[ Extern ] Froms (file memcpy.c, line 162)
+[ Extern ] Froms (file memcpy.c, line 166)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
---- Properties of Function 'main_uninit'
+--- Properties of Function 'test_uninit'
--------------------------------------------------------------------------------
-[ Valid ] Assertion (file memcpy.c, line 173)
+[ Valid ] Assertion (file memcpy.c, line 177)
by Eva.
-[ Valid ] Assertion (file memcpy.c, line 175)
+[ Valid ] Assertion (file memcpy.c, line 179)
by Eva.
-[ Valid ] Assertion (file memcpy.c, line 180)
+[ Valid ] Assertion (file memcpy.c, line 184)
by Eva.
-[ Valid ] Assertion (file memcpy.c, line 188)
+[ Valid ] Assertion (file memcpy.c, line 192)
by Eva.
-[ Valid ] Assertion (file memcpy.c, line 191)
+[ Valid ] Assertion (file memcpy.c, line 195)
by Eva.
-[ Valid ] Assertion (file memcpy.c, line 199)
+[ Valid ] Assertion (file memcpy.c, line 203)
by Eva.
-[ - ] Assertion 'Eva,initialization' (file memcpy.c, line 182)
+[ - ] Assertion 'Eva,initialization' (file memcpy.c, line 186)
tried with Eva.
-[ - ] Assertion 'Eva,initialization' (file memcpy.c, line 192)
+[ - ] Assertion 'Eva,initialization' (file memcpy.c, line 196)
tried with Eva.
-[ - ] Assertion 'Eva,initialization' (file memcpy.c, line 201)
+[ - ] Assertion 'Eva,initialization' (file memcpy.c, line 205)
tried with Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 172)
+[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 176)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 172)
+[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 176)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 172)
+[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 176)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 174)
+[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 178)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 174)
+[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 178)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 174)
+[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 178)
by Eva.
-[ Valid ] Instance of 'Pre-condition (file memcpy.c, line 161)' at call 'make_unknown' (file memcpy.c, line 178)
+[ Valid ] Instance of 'Pre-condition (file memcpy.c, line 165)' at call 'make_unknown' (file memcpy.c, line 182)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 179)
+[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 183)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 179)
+[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 183)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 179)
+[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 183)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 181)
+[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 185)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 181)
+[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 185)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 181)
+[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 185)
by Eva.
-[ Valid ] Instance of 'Pre-condition (file memcpy.c, line 161)' at call 'make_unknown' (file memcpy.c, line 185)
+[ Valid ] Instance of 'Pre-condition (file memcpy.c, line 165)' at call 'make_unknown' (file memcpy.c, line 189)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 187)
+[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 191)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 187)
+[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 191)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 187)
+[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 191)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 190)
+[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 194)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 190)
+[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 194)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 190)
+[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 194)
by Eva.
-[ Valid ] Instance of 'Pre-condition (file memcpy.c, line 161)' at call 'make_unknown' (file memcpy.c, line 196)
+[ Valid ] Instance of 'Pre-condition (file memcpy.c, line 165)' at call 'make_unknown' (file memcpy.c, line 200)
by Eva.
-[ Valid ] Instance of 'Pre-condition (file memcpy.c, line 161)' at call 'make_unknown' (file memcpy.c, line 197)
+[ Valid ] Instance of 'Pre-condition (file memcpy.c, line 165)' at call 'make_unknown' (file memcpy.c, line 201)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 198)
+[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 202)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 198)
+[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 202)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 198)
+[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 202)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 200)
+[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 204)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 200)
+[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 204)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 200)
+[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 204)
by Eva.
--------------------------------------------------------------------------------
---- Properties of Function 'main_local'
+--- Properties of Function 'test_local'
--------------------------------------------------------------------------------
-[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 209)
+[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 213)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 209)
+[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 213)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 209)
+[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 213)
by Eva.
@@ -2228,24 +2185,22 @@
--- Properties of Function 'copy_0'
--------------------------------------------------------------------------------
-[ Alarm ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 220)
+[ - ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 221)
- By Eva, with pending:
- - Unreachable call 'memcpy' (file memcpy.c, line 220)
-[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 220)
+ tried with Eva.
+[ Valid ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 221)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 220)
+[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 221)
by Eva.
-[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 221)
+[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file memcpy.c, line 222)
by Eva.
-[ Alarm ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 221)
+[ - ] Instance of 'Pre-condition 'valid_src'' at call 'memcpy' (file memcpy.c, line 222)
- By Eva, with pending:
- - Unreachable call 'memcpy' (file memcpy.c, line 221)
-[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 221)
+ tried with Eva.
+[ Valid ] Instance of 'Pre-condition 'separation'' at call 'memcpy' (file memcpy.c, line 222)
by Eva.
@@ -2255,7 +2210,6 @@
169 Completely validated
1 Locally validated
267 Considered valid
- 32 To be validated
- 4 Alarms emitted
+ 36 To be validated
473 Total
--------------------------------------------------------------------------------
diff --git a/tests/builtins/oracle/memcpy.1.res.oracle b/tests/builtins/oracle/memcpy.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..ebc79e7b2b76d346d631bbed3cc96636ade6477b
--- /dev/null
+++ b/tests/builtins/oracle/memcpy.1.res.oracle
@@ -0,0 +1,56 @@
+[kernel] Parsing memcpy.c (with preprocessing)
+[eva] Analyzing a complete application starting at copy_0
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ NULL[rbits 800000 to 800015] ∈ [--..--]
+ i ∈ [--..--]
+ src[0..19] ∈ {0}
+ dst1[0..19] ∈ {0}
+ dst2[0..19] ∈ {0}
+ dst3[0..19] ∈ {0}
+ dst4[0..19] ∈ {0}
+ dst5[0..99] ∈ {0}
+ maybe ∈ [--..--]
+ tm[0..999] ∈ {0}
+ um[0..999] ∈ {0}
+ ttyp[0..999] ∈ {0}
+ v1 ∈ {0}
+ v2 ∈ {0}
+ v3 ∈ {0}
+ v4 ∈ {0}
+ v5 ∈ {0}
+ t[0..3] ∈ {0}
+[eva] memcpy.c:221: Call to builtin memcpy
+[eva:alarm] memcpy.c:221: Warning:
+ function memcpy: precondition 'valid_dest' got status invalid.
+[eva] memcpy.c:221:
+ function memcpy: no state left, precondition 'valid_src' got status valid.
+[eva] memcpy.c:221:
+ function memcpy: no state left, precondition 'separation' got status valid.
+[eva] memcpy.c:222: Call to builtin memcpy
+[eva] memcpy.c:222: function memcpy: precondition 'valid_dest' got status valid.
+[eva:alarm] memcpy.c:222: Warning:
+ function memcpy: precondition 'valid_src' got status invalid.
+[eva] memcpy.c:222:
+ function memcpy: no state left, precondition 'separation' got status valid.
+[eva] Recording results for copy_0
+[eva] Done for function copy_0
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function copy_0:
+
+[from] Computing for function copy_0
+[from] Computing for function memcpy <-copy_0
+[from] Done for function memcpy
+[from] Done for function copy_0
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function memcpy:
+ \result FROM dest
+[from] Function copy_0:
+ NO EFFECTS
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function copy_0:
+ \nothing
+[inout] Inputs for function copy_0:
+ i
diff --git a/tests/builtins/oracle_gauges/memcpy.0.res.oracle b/tests/builtins/oracle_gauges/memcpy.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..5e4fbca1c4a14c624435c5b4d0c53eded4b69870
--- /dev/null
+++ b/tests/builtins/oracle_gauges/memcpy.0.res.oracle
@@ -0,0 +1,5 @@
+145a146,147
+> [eva] memcpy.c:100: Call to builtin memcpy
+> [eva] memcpy.c:100: Call to builtin memcpy
+367a370
+> [eva] memcpy.c:231: starting to merge loop iterations
diff --git a/tests/builtins/oracle_gauges/memcpy.res.oracle b/tests/builtins/oracle_gauges/memcpy.res.oracle
deleted file mode 100644
index a770a6bfa690f6889cc7840880cba52333ba7fbe..0000000000000000000000000000000000000000
--- a/tests/builtins/oracle_gauges/memcpy.res.oracle
+++ /dev/null
@@ -1,5 +0,0 @@
-146a147,148
-> [eva] memcpy.c:96: Call to builtin memcpy
-> [eva] memcpy.c:96: Call to builtin memcpy
-372a375
-> [eva] memcpy.c:230: starting to merge loop iterations
diff --git a/tests/syntax/array_size.c b/tests/syntax/array_size.c
new file mode 100644
index 0000000000000000000000000000000000000000..89bec6ef204ad5945c9caf79d316c5b8cef37eb0
--- /dev/null
+++ b/tests/syntax/array_size.c
@@ -0,0 +1,39 @@
+/* run.config*
+ EXIT: 1
+ OPT: -cpp-extra-args="-DNEG_SIZE"
+ OPT: -cpp-extra-args="-DVLA_INIT1"
+ OPT: -cpp-extra-args="-DVLA_INIT2"
+ OPT: -cpp-extra-args="-DVLA_GLOB1"
+ OPT: -cpp-extra-args="-DVLA_GLOB2"
+ OPT: -cpp-extra-args="-DVLA_STRUCT"
+*/
+
+#ifdef NEG_SIZE
+int f(int t[-1]) { return t[0]; } // should raise an error
+#endif
+
+#ifdef VLA_INIT1
+void g(int size) {
+ int a[size] = { 0 }; // error: VLA can't be initialized
+}
+#endif
+
+#ifdef VLA_INIT2
+void h (int size) {
+ int a [size][2] = { { 0 } }; // same as above
+}
+#endif
+
+const int size = 42;
+
+#ifdef VLA_GLOB1
+int a[size]; // error: global arrays must have a fixed size.
+#endif
+
+#ifdef VLA_GLOB2
+int a[2][size]; // same as above
+#endif
+
+#ifdef VLA_STRUCT
+struct { int a [size]; }; // error: no VLA in struct
+#endif
diff --git a/tests/syntax/array_size.i b/tests/syntax/array_size.i
deleted file mode 100644
index e8d46d0178a748a46145d63601c3f5ba9b1711af..0000000000000000000000000000000000000000
--- a/tests/syntax/array_size.i
+++ /dev/null
@@ -1,7 +0,0 @@
-/* run.config*
- EXIT: 1
- STDOPT:
-*/
-
-
-int f(int t[-1]) { return t[0]; } // should raise an error
diff --git a/tests/syntax/generic.c b/tests/syntax/generic.c
index 17726aab534ca3727bd74b063ccb58fd833d160c..15a9d6aa05fa9e4048c736354908ca4f41fe01bc 100644
--- a/tests/syntax/generic.c
+++ b/tests/syntax/generic.c
@@ -9,6 +9,7 @@
STDOPT: #"-cpp-extra-args=-DINCOMPLETE_TYPE"
STDOPT: #"-cpp-extra-args=-DINCOMPATIBLE_QUALIFIED_TYPE"
STDOPT: #"-cpp-extra-args=-DFUNCTION_TYPE"
+ STDOPT: #"-cpp-extra-args=-DVLA"
EXIT: 0
STDOPT:
*/
@@ -63,6 +64,11 @@ int main() {
#endif
#ifdef INCOMPATIBLE_QUALIFIED_TYPE
int a = _Generic("abc", char const *: 0);
+#endif
+#ifdef VLA
+ int x = 42;
+ int y[x];
+ int a = _Generic(y, int[x]: 0, default: 1);
#endif
int ok1 = _Generic("abc", char*: 0);
int ok2 = _Generic(1.0, float: 1, double: 0);
diff --git a/tests/syntax/oracle/array_size.0.res.oracle b/tests/syntax/oracle/array_size.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..fea23a0a0938e75b5581885fc29989ef383e0b94
--- /dev/null
+++ b/tests/syntax/oracle/array_size.0.res.oracle
@@ -0,0 +1,5 @@
+[kernel] Parsing array_size.c (with preprocessing)
+[kernel] array_size.c:12: User Error: Array length is negative.
+[kernel] User Error: stopping on file "array_size.c" that has errors. Add '-kernel-msg-key pp'
+ for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/array_size.1.res.oracle b/tests/syntax/oracle/array_size.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..2cc9bdd172ac6d1eb750d7eca455cab9eba055b9
--- /dev/null
+++ b/tests/syntax/oracle/array_size.1.res.oracle
@@ -0,0 +1,6 @@
+[kernel] Parsing array_size.c (with preprocessing)
+[kernel] array_size.c:17: User Error:
+ Variable-sized array cannot have initializer
+[kernel] User Error: stopping on file "array_size.c" that has errors. Add '-kernel-msg-key pp'
+ for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/array_size.2.res.oracle b/tests/syntax/oracle/array_size.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..fbc09a34ed2aa0b72b59478a488aefe0399326f1
--- /dev/null
+++ b/tests/syntax/oracle/array_size.2.res.oracle
@@ -0,0 +1,6 @@
+[kernel] Parsing array_size.c (with preprocessing)
+[kernel] array_size.c:23: User Error:
+ Variable-sized array cannot have initializer
+[kernel] User Error: stopping on file "array_size.c" that has errors. Add '-kernel-msg-key pp'
+ for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/array_size.3.res.oracle b/tests/syntax/oracle/array_size.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..421d4380a6e78931a60d1830933bb337ae95e7b2
--- /dev/null
+++ b/tests/syntax/oracle/array_size.3.res.oracle
@@ -0,0 +1,5 @@
+[kernel] Parsing array_size.c (with preprocessing)
+[kernel] array_size.c:30: User Error: Global arrays cannot have variable size
+[kernel] User Error: stopping on file "array_size.c" that has errors. Add '-kernel-msg-key pp'
+ for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/array_size.4.res.oracle b/tests/syntax/oracle/array_size.4.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..f18504df1ed797cc2f0f886c37a9da1edc893068
--- /dev/null
+++ b/tests/syntax/oracle/array_size.4.res.oracle
@@ -0,0 +1,5 @@
+[kernel] Parsing array_size.c (with preprocessing)
+[kernel] array_size.c:34: User Error: Global arrays cannot have variable size
+[kernel] User Error: stopping on file "array_size.c" that has errors. Add '-kernel-msg-key pp'
+ for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/array_size.5.res.oracle b/tests/syntax/oracle/array_size.5.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..d308118b0fb6595ecb48fe215c0be5a62fd29934
--- /dev/null
+++ b/tests/syntax/oracle/array_size.5.res.oracle
@@ -0,0 +1,6 @@
+[kernel] Parsing array_size.c (with preprocessing)
+[kernel] array_size.c:38: User Error:
+ "Variable length array in structure" extension is not supported
+[kernel] User Error: stopping on file "array_size.c" that has errors. Add '-kernel-msg-key pp'
+ for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/array_size.res.oracle b/tests/syntax/oracle/array_size.res.oracle
deleted file mode 100644
index ea94c308541ab9a6e185a5411e3df9086a762ef4..0000000000000000000000000000000000000000
--- a/tests/syntax/oracle/array_size.res.oracle
+++ /dev/null
@@ -1,4 +0,0 @@
-[kernel] Parsing array_size.i (no preprocessing)
-[kernel] array_size.i:7: User Error: Array length is negative.
-[kernel] User Error: stopping on file "array_size.i" that has errors.
-[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/generic.1.res.oracle b/tests/syntax/oracle/generic.1.res.oracle
index c8f6605be6dcb690f616c3dd9bcdf7fc7226ea19..525bed32e1ea201e2fd17042f1b7055ef57eaa50 100644
--- a/tests/syntax/oracle/generic.1.res.oracle
+++ b/tests/syntax/oracle/generic.1.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing generic.c (with preprocessing)
-[kernel] generic.c:36:
+[kernel] generic.c:37:
_Generic requires at least one generic association:
- Location: line 36, between columns 10 and 25, before or at token: ;
- 34 int main() {
- 35 #ifdef NONE
- 36 int a = _Generic("abc");
+ Location: line 37, between columns 10 and 25, before or at token: ;
+ 35 int main() {
+ 36 #ifdef NONE
+ 37 int a = _Generic("abc");
^^^^^^^^^^^^^^^
- 37 #endif
- 38 #ifdef TOO_MANY_DEFAULTS
+ 38 #endif
+ 39 #ifdef TOO_MANY_DEFAULTS
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/generic.10.res.oracle b/tests/syntax/oracle/generic.10.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..70bdefa20fded77f7906a06abef980f36e8fc77e
--- /dev/null
+++ b/tests/syntax/oracle/generic.10.res.oracle
@@ -0,0 +1,32 @@
+[kernel] Parsing generic.c (with preprocessing)
+/* Generated by Frama-C */
+int foo(int i)
+{
+ int __retres;
+ __retres = 0;
+ return __retres;
+}
+
+void void_foo(int i)
+{
+ return;
+}
+
+float cbrtf(float x);
+
+int main(void)
+{
+ int __retres;
+ float tmp;
+ int ok1 = 0;
+ int ok2 = 0;
+ int ok3 = 0;
+ int ok4 = 0;
+ tmp = cbrtf(0.0f);
+ double c = (double)tmp;
+ int ok5 = 0;
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/tests/syntax/oracle/generic.2.res.oracle b/tests/syntax/oracle/generic.2.res.oracle
index 0edc5626dfd5157572f29d022cfbf997a14fba98..592f81d34ca92c28b5b06208ad9812a2b163f9de 100644
--- a/tests/syntax/oracle/generic.2.res.oracle
+++ b/tests/syntax/oracle/generic.2.res.oracle
@@ -1,10 +1,10 @@
[kernel] Parsing generic.c (with preprocessing)
-[kernel] generic.c:39: User Error:
+[kernel] generic.c:40: User Error:
multiple default clauses in _Generic selection
- 37 #endif
- 38 #ifdef TOO_MANY_DEFAULTS
- 39 int a = _Generic("abc", default: 1, default: 1);
+ 38 #endif
+ 39 #ifdef TOO_MANY_DEFAULTS
+ 40 int a = _Generic("abc", default: 1, default: 1);
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- 40 #endif
- 41 #ifdef TOO_MANY_COMPATIBLE
+ 41 #endif
+ 42 #ifdef TOO_MANY_COMPATIBLE
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/generic.3.res.oracle b/tests/syntax/oracle/generic.3.res.oracle
index af00e69e6f9a9db9d0453d3965d5af3f92f4deb1..89f860800fa257cb2642325739dc2d86ca8c1624 100644
--- a/tests/syntax/oracle/generic.3.res.oracle
+++ b/tests/syntax/oracle/generic.3.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing generic.c (with preprocessing)
-[kernel] generic.c:43: User Error:
+[kernel] generic.c:44: User Error:
multiple compatible types in _Generic selection:
'my_uint' and 'unsigned int'
- 41 #ifdef TOO_MANY_COMPATIBLE
- 42 // compatibility via typedef
- 43 int a = _Generic(42, my_uint: 1, unsigned int: 2);
+ 42 #ifdef TOO_MANY_COMPATIBLE
+ 43 // compatibility via typedef
+ 44 int a = _Generic(42, my_uint: 1, unsigned int: 2);
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- 44 #endif
- 45 #ifdef TOO_MANY_COMPATIBLE2
+ 45 #endif
+ 46 #ifdef TOO_MANY_COMPATIBLE2
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/generic.4.res.oracle b/tests/syntax/oracle/generic.4.res.oracle
index 4dea267e9f5cf04b162f789e3847a6714d99c8a0..3b8bc64668e46d3130dbeadd94f7436883f59ddb 100644
--- a/tests/syntax/oracle/generic.4.res.oracle
+++ b/tests/syntax/oracle/generic.4.res.oracle
@@ -1,14 +1,14 @@
[kernel] Parsing generic.c (with preprocessing)
-[kernel] generic.c:47: User Error:
+[kernel] generic.c:48: User Error:
multiple compatible types in _Generic selection:
'void (*)()' and 'void (*)(void)'
- 45 #ifdef TOO_MANY_COMPATIBLE2
- 46 // compatibility modulo implicit arguments
+ 46 #ifdef TOO_MANY_COMPATIBLE2
+ 47 // compatibility modulo implicit arguments
- 47 int a = _Generic(0,
- 48 void (*)(): 0,
- 49 void (*)(void): 0);
+ 48 int a = _Generic(0,
+ 49 void (*)(): 0,
+ 50 void (*)(void): 0);
- 50 #endif
- 51 #ifdef TOO_MANY_COMPATIBLE3
+ 51 #endif
+ 52 #ifdef TOO_MANY_COMPATIBLE3
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/generic.5.res.oracle b/tests/syntax/oracle/generic.5.res.oracle
index 579b9dde7959145550bcea41382a8e721f40b21d..5c1e7279049cc649936e472d3b2b116f1eb5d75f 100644
--- a/tests/syntax/oracle/generic.5.res.oracle
+++ b/tests/syntax/oracle/generic.5.res.oracle
@@ -1,15 +1,15 @@
[kernel] Parsing generic.c (with preprocessing)
-[kernel] generic.c:54: User Error:
+[kernel] generic.c:55: User Error:
controlling expression compatible with more than one association type in _Generic selection:
controlling expression: '(void (*)())0' (type: void (*)());
compatible types: void (*)(void), void (*)(int )
- 52 // implicit arguments compatible between first and second selector,
- 53 // but the selectors themselves are not compatible between them
+ 53 // implicit arguments compatible between first and second selector,
+ 54 // but the selectors themselves are not compatible between them
- 54 int a = _Generic((void (*)()) 0,
- 55 void (*)(int): 0,
- 56 void (*)(void): 0);
+ 55 int a = _Generic((void (*)()) 0,
+ 56 void (*)(int): 0,
+ 57 void (*)(void): 0);
- 57 #endif
- 58 #ifdef INCOMPLETE_TYPE
+ 58 #endif
+ 59 #ifdef INCOMPLETE_TYPE
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/generic.6.res.oracle b/tests/syntax/oracle/generic.6.res.oracle
index fbfffc1be280933ec883e33e343a303d4541dd09..c53dd9c2738d9895b66b26f0f716fc193b587cc6 100644
--- a/tests/syntax/oracle/generic.6.res.oracle
+++ b/tests/syntax/oracle/generic.6.res.oracle
@@ -1,10 +1,10 @@
[kernel] Parsing generic.c (with preprocessing)
-[kernel] generic.c:59: User Error:
+[kernel] generic.c:60: User Error:
generic association with incomplete type 'void'
- 57 #endif
- 58 #ifdef INCOMPLETE_TYPE
- 59 int a = _Generic(42, void: 1, default: 2);
+ 58 #endif
+ 59 #ifdef INCOMPLETE_TYPE
+ 60 int a = _Generic(42, void: 1, default: 2);
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- 60 #endif
- 61 #ifdef FUNCTION_TYPE
+ 61 #endif
+ 62 #ifdef FUNCTION_TYPE
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/generic.7.res.oracle b/tests/syntax/oracle/generic.7.res.oracle
index c232c3c417e6f8d49a53f25f9f116dc939d908b2..03f063c8583744504a73b16416ccd9bf9269d900 100644
--- a/tests/syntax/oracle/generic.7.res.oracle
+++ b/tests/syntax/oracle/generic.7.res.oracle
@@ -1,12 +1,12 @@
[kernel] Parsing generic.c (with preprocessing)
-[kernel] generic.c:65: User Error:
+[kernel] generic.c:66: User Error:
no compatible types and no default type in _Generic selection:
controlling expression: '"abc"' (type: char *);
candidate types: char const *
- 63 #endif
- 64 #ifdef INCOMPATIBLE_QUALIFIED_TYPE
- 65 int a = _Generic("abc", char const *: 0);
+ 64 #endif
+ 65 #ifdef INCOMPATIBLE_QUALIFIED_TYPE
+ 66 int a = _Generic("abc", char const *: 0);
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- 66 #endif
- 67 int ok1 = _Generic("abc", char*: 0);
+ 67 #endif
+ 68 #ifdef VLA
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/generic.8.res.oracle b/tests/syntax/oracle/generic.8.res.oracle
index fe35717281298c85c4a8ef02888473d4a3b90dce..78569285df29b0e24c4d302c3e8ec06023d6ca9c 100644
--- a/tests/syntax/oracle/generic.8.res.oracle
+++ b/tests/syntax/oracle/generic.8.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing generic.c (with preprocessing)
-[kernel] generic.c:62:
+[kernel] generic.c:63:
syntax error:
- Location: line 62, column 27, before or at token: int
- 60 #endif
- 61 #ifdef FUNCTION_TYPE
- 62 int a = _Generic(1, void(int): 1);
+ Location: line 63, column 27, before or at token: int
+ 61 #endif
+ 62 #ifdef FUNCTION_TYPE
+ 63 int a = _Generic(1, void(int): 1);
^
- 63 #endif
- 64 #ifdef INCOMPATIBLE_QUALIFIED_TYPE
+ 64 #endif
+ 65 #ifdef INCOMPATIBLE_QUALIFIED_TYPE
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/generic.9.res.oracle b/tests/syntax/oracle/generic.9.res.oracle
index 70bdefa20fded77f7906a06abef980f36e8fc77e..ef373d91c17e019395537108fc0b5d486723d6a9 100644
--- a/tests/syntax/oracle/generic.9.res.oracle
+++ b/tests/syntax/oracle/generic.9.res.oracle
@@ -1,32 +1,10 @@
[kernel] Parsing generic.c (with preprocessing)
-/* Generated by Frama-C */
-int foo(int i)
-{
- int __retres;
- __retres = 0;
- return __retres;
-}
-
-void void_foo(int i)
-{
- return;
-}
-
-float cbrtf(float x);
-
-int main(void)
-{
- int __retres;
- float tmp;
- int ok1 = 0;
- int ok2 = 0;
- int ok3 = 0;
- int ok4 = 0;
- tmp = cbrtf(0.0f);
- double c = (double)tmp;
- int ok5 = 0;
- __retres = 0;
- return __retres;
-}
-
-
+[kernel] generic.c:71: User Error:
+ generic association with variably modified type 'int [x]'
+ 69 int x = 42;
+ 70 int y[x];
+ 71 int a = _Generic(y, int[x]: 0, default: 1);
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ 72 #endif
+ 73 int ok1 = _Generic("abc", char*: 0);
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/sizeof.0.res.oracle b/tests/syntax/oracle/sizeof.0.res.oracle
index aa1ba789ca9fca267ec802decd82a0ed1c226e9d..4eb800ca12dab45e1da5907e8bb2d64eaaca7983 100644
--- a/tests/syntax/oracle/sizeof.0.res.oracle
+++ b/tests/syntax/oracle/sizeof.0.res.oracle
@@ -1,5 +1,6 @@
[kernel] Parsing sizeof.c (with preprocessing)
/* Generated by Frama-C */
+#include "assert.h"
#include "stdint.h"
char c = (char)1;
char a = (char)'a';
@@ -14,4 +15,12 @@ uint64_t u64 = 6453UL;
int v = 645201;
float f = (float)1.;
double d = 1.;
+void vla(int n)
+{
+ unsigned long s = sizeof(int [n]);
+ __FC_assert((s == (unsigned long)n * sizeof(int)) != 0,"sizeof.c",49,
+ "s == n * sizeof(int)");
+ return;
+}
+
diff --git a/tests/syntax/oracle/sizeof.1.res.oracle b/tests/syntax/oracle/sizeof.1.res.oracle
index 05c8abe3fa6d930520097aa9c3b94a8f07000f3e..f66dc175d39c9a6d08950bd025d00bf455a6c564 100644
--- a/tests/syntax/oracle/sizeof.1.res.oracle
+++ b/tests/syntax/oracle/sizeof.1.res.oracle
@@ -1,5 +1,6 @@
[kernel] Parsing sizeof.c (with preprocessing)
/* Generated by Frama-C */
+#include "assert.h"
#include "stdint.h"
char c = (char)1;
char a = (char)'a';
@@ -14,4 +15,12 @@ uint64_t u64 = 6453ULL;
int v = 645201;
float f = (float)1.;
double d = 1.;
+void vla(int n)
+{
+ unsigned long s = (unsigned long)sizeof(int [n]);
+ __FC_assert((s == (unsigned long)((unsigned int)n * sizeof(int))) != 0,
+ "sizeof.c",49,"s == n * sizeof(int)");
+ return;
+}
+
diff --git a/tests/syntax/oracle/vla_multidim.1.res.oracle b/tests/syntax/oracle/vla_multidim.1.res.oracle
index 09f9c527f3c5e955e651df57f5b5967bba4f1a8a..aa97a0bb5c6ca726925a4e3bc7ac37cb9fc1c8af 100644
--- a/tests/syntax/oracle/vla_multidim.1.res.oracle
+++ b/tests/syntax/oracle/vla_multidim.1.res.oracle
@@ -1,13 +1,4 @@
[kernel] Parsing vla_multidim.c (with preprocessing)
-[kernel] vla_multidim.c:15: User Error:
- Array length n is not a compile-time constant,
- and currently VLAs may only have their first dimension as variable.
-[kernel] vla_multidim.c:16: User Error:
- Array length n is not a compile-time constant,
- and currently VLAs may only have their first dimension as variable.
-[kernel] vla_multidim.c:17: User Error:
- Array length n is not a compile-time constant,
- and currently VLAs may only have their first dimension as variable.
-[kernel] User Error: stopping on file "vla_multidim.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Frama-C aborted: unimplemented feature.
+ You may send a feature request at https://git.frama-c.com/pub/frama-c/issues with:
+ '[Frama-C] For multi-dimensional arrays, variable length is only supported on the first dimension'.
diff --git a/tests/syntax/oracle/vla_multidim.2.res.oracle b/tests/syntax/oracle/vla_multidim.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..aa97a0bb5c6ca726925a4e3bc7ac37cb9fc1c8af
--- /dev/null
+++ b/tests/syntax/oracle/vla_multidim.2.res.oracle
@@ -0,0 +1,4 @@
+[kernel] Parsing vla_multidim.c (with preprocessing)
+[kernel] Frama-C aborted: unimplemented feature.
+ You may send a feature request at https://git.frama-c.com/pub/frama-c/issues with:
+ '[Frama-C] For multi-dimensional arrays, variable length is only supported on the first dimension'.
diff --git a/tests/syntax/oracle/vla_multidim.3.res.oracle b/tests/syntax/oracle/vla_multidim.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..aa97a0bb5c6ca726925a4e3bc7ac37cb9fc1c8af
--- /dev/null
+++ b/tests/syntax/oracle/vla_multidim.3.res.oracle
@@ -0,0 +1,4 @@
+[kernel] Parsing vla_multidim.c (with preprocessing)
+[kernel] Frama-C aborted: unimplemented feature.
+ You may send a feature request at https://git.frama-c.com/pub/frama-c/issues with:
+ '[Frama-C] For multi-dimensional arrays, variable length is only supported on the first dimension'.
diff --git a/tests/syntax/sizeof.c b/tests/syntax/sizeof.c
index a27bf94011e4a4341faf3a7e948d360ce70ec2d4..7fbc16abc9fc42a0b75856d8b054f318582f9da1 100644
--- a/tests/syntax/sizeof.c
+++ b/tests/syntax/sizeof.c
@@ -3,6 +3,9 @@
STDOPT: -machdep x86_64
STDOPT: -machdep x86_32
*/
+
+#include <assert.h>
+
char c = 1;
_Static_assert(sizeof(-c) == sizeof(int), "Integer promotion with minus");
_Static_assert(sizeof(+c) == sizeof(int), "Integer promotion with plus");
@@ -40,3 +43,8 @@ float f = 1.;
_Static_assert(sizeof +f == sizeof(float), "Float promotion");
double d = 1.;
_Static_assert(sizeof +d == sizeof(double), "Double promotion");
+
+void vla(int n) {
+ unsigned long s = sizeof(int[n]);
+ assert(s == n * sizeof(int));
+}
diff --git a/tests/syntax/vla_multidim.c b/tests/syntax/vla_multidim.c
index 8308e0483842a31af16107b276f1398642f3acdf..e2c6c75e21bf1e03b0a0188067399a74cb67bbec 100644
--- a/tests/syntax/vla_multidim.c
+++ b/tests/syntax/vla_multidim.c
@@ -1,7 +1,9 @@
/* run.config
STDOPT: #""
- EXIT: 1
- STDOPT: #"-cpp-extra-args=-DMULTIVLA"
+ EXIT: 3
+ STDOPT: #"-cpp-extra-args=-DMULTIVLA1"
+ STDOPT: #"-cpp-extra-args=-DMULTIVLA2"
+ STDOPT: #"-cpp-extra-args=-DMULTIVLA3"
*/
const int n = 10;
@@ -10,10 +12,15 @@ void main() {
int a[n][42]; // single variable length dimension
a[0][0] = 1;
int b[a[0][0]][5][10]; // idem
-#ifdef MULTIVLA
- // arrays with non-first variable dimensions; not currently supported
+
+// arrays with non-first variable dimensions; not currently supported
+#ifdef MULTIVLA1
int c[n][n];
- int d[42][n];
+#endif
+#ifdef MULTIVLA2
+int d[42][n];
+#endif
+#ifdef MULTIVLA3
int e[1][n][9];
#endif
}
diff --git a/tests/value/oracle_multidim/strings_logic.res.oracle b/tests/value/oracle_multidim/strings_logic.res.oracle
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000