diff --git a/share/libc/__fc_builtin.h b/share/libc/__fc_builtin.h
index fa8e9c3a759d4c58282e4382453bcf44d4e641ab..35e11be02df89bac2af9b79c5f22ae5bb0ff7414 100644
--- a/share/libc/__fc_builtin.h
+++ b/share/libc/__fc_builtin.h
@@ -35,118 +35,124 @@ extern volatile int Frama_C_entropy_source __attribute__((unused));
assigns Frama_C_entropy_source \from Frama_C_entropy_source;
ensures initialization: \initialized(p + (0 .. l-1));
*/
-extern void Frama_C_make_unknown(char *p, size_t l);
+extern void Frama_C_make_unknown(char *p, size_t l) __attribute__((FC_BUILTIN));
/*@ assigns \result \from a, b, Frama_C_entropy_source;
assigns Frama_C_entropy_source \from Frama_C_entropy_source;
ensures result_a_or_b: \result == a || \result == b ;
*/
-extern int Frama_C_nondet(int a, int b);
+extern int Frama_C_nondet(int a, int b) __attribute__((FC_BUILTIN));
/*@ assigns \result \from a, b, Frama_C_entropy_source;
assigns Frama_C_entropy_source \from Frama_C_entropy_source;
ensures result_a_or_b: \result == a || \result == b ;
*/
-extern void *Frama_C_nondet_ptr(void *a, void *b);
+extern void *Frama_C_nondet_ptr(void *a, void *b) __attribute__((FC_BUILTIN));
/*@ requires order: min <= max;
assigns \result \from min, max, Frama_C_entropy_source;
assigns Frama_C_entropy_source \from Frama_C_entropy_source;
ensures result_bounded: min <= \result <= max ;
*/
-extern int Frama_C_interval(int min, int max);
+extern int Frama_C_interval(int min, int max) __attribute__((FC_BUILTIN));
/*@ requires order: min <= max;
assigns \result \from min, max, Frama_C_entropy_source;
assigns Frama_C_entropy_source \from Frama_C_entropy_source;
ensures result_bounded: min <= \result <= max ;
*/
-extern int Frama_C_interval_split(int min, int max);
+extern int Frama_C_interval_split(int min, int max) __attribute__((FC_BUILTIN));
/*@ requires order: min <= max;
assigns \result \from min, max, Frama_C_entropy_source;
assigns Frama_C_entropy_source \from Frama_C_entropy_source;
ensures result_bounded: min <= \result <= max ;
*/
-extern unsigned char Frama_C_unsigned_char_interval
- (unsigned char min, unsigned char max);
+extern unsigned char Frama_C_unsigned_char_interval(unsigned char min,
+ unsigned char max)
+ __attribute__((FC_BUILTIN));
/*@ requires order: min <= max;
assigns \result \from min, max, Frama_C_entropy_source;
assigns Frama_C_entropy_source \from Frama_C_entropy_source;
ensures result_bounded: min <= \result <= max ;
*/
-extern char Frama_C_char_interval(char min, char max);
+extern char Frama_C_char_interval(char min, char max)
+ __attribute__((FC_BUILTIN));
/*@ requires order: min <= max;
assigns \result \from min, max, Frama_C_entropy_source;
assigns Frama_C_entropy_source \from Frama_C_entropy_source;
ensures result_bounded: min <= \result <= max ;
*/
-extern unsigned short Frama_C_unsigned_short_interval(unsigned short min, unsigned short max);
+extern unsigned short Frama_C_unsigned_short_interval(unsigned short min,
+ unsigned short max)
+ __attribute__((FC_BUILTIN));
/*@ requires order: min <= max;
assigns \result \from min, max, Frama_C_entropy_source;
assigns Frama_C_entropy_source \from Frama_C_entropy_source;
ensures result_bounded: min <= \result <= max ;
*/
-extern short Frama_C_short_interval(short min, short max);
-
+extern short Frama_C_short_interval(short min, short max)
+ __attribute__((FC_BUILTIN));
/*@ requires order: min <= max;
assigns \result \from min, max, Frama_C_entropy_source;
assigns Frama_C_entropy_source \from Frama_C_entropy_source;
ensures result_bounded: min <= \result <= max ;
*/
-extern unsigned int Frama_C_unsigned_int_interval(unsigned int min, unsigned int max);
+extern unsigned int Frama_C_unsigned_int_interval(unsigned int min,
+ unsigned int max)
+ __attribute__((FC_BUILTIN));
/*@ requires order: min <= max;
assigns \result \from min, max, Frama_C_entropy_source;
assigns Frama_C_entropy_source \from Frama_C_entropy_source;
ensures result_bounded: min <= \result <= max ;
*/
-extern int Frama_C_int_interval(int min, int max);
-
+extern int Frama_C_int_interval(int min, int max) __attribute__((FC_BUILTIN));
/*@ requires order: min <= max;
assigns \result \from min, max, Frama_C_entropy_source;
assigns Frama_C_entropy_source \from Frama_C_entropy_source;
ensures result_bounded: min <= \result <= max ;
*/
-extern unsigned long Frama_C_unsigned_long_interval
- (unsigned long min, unsigned long max);
+extern unsigned long Frama_C_unsigned_long_interval(unsigned long min,
+ unsigned long max)
+ __attribute__((FC_BUILTIN));
/*@ requires order: min <= max;
assigns \result \from min, max, Frama_C_entropy_source;
assigns Frama_C_entropy_source \from Frama_C_entropy_source;
ensures result_bounded: min <= \result <= max ;
*/
-extern long Frama_C_long_interval(long min, long max);
-
+extern long Frama_C_long_interval(long min, long max)
+ __attribute__((FC_BUILTIN));
/*@ requires order: min <= max;
assigns \result \from min, max, Frama_C_entropy_source;
assigns Frama_C_entropy_source \from Frama_C_entropy_source;
ensures result_bounded: min <= \result <= max ;
*/
-extern unsigned long long Frama_C_unsigned_long_long_interval
- (unsigned long long min, unsigned long long max);
+extern unsigned long long Frama_C_unsigned_long_long_interval(
+ unsigned long long min, unsigned long long max) __attribute__((FC_BUILTIN));
/*@ requires order: min <= max;
assigns \result \from min, max, Frama_C_entropy_source;
assigns Frama_C_entropy_source \from Frama_C_entropy_source;
ensures result_bounded: min <= \result <= max ;
*/
-extern long long Frama_C_long_long_interval(long long min, long long max);
-
+extern long long Frama_C_long_long_interval(long long min, long long max)
+ __attribute__((FC_BUILTIN));
/*@ requires order: min <= max;
assigns \result \from min, max, Frama_C_entropy_source;
assigns Frama_C_entropy_source \from Frama_C_entropy_source;
ensures result_bounded: min <= \result <= max ;
*/
-extern size_t Frama_C_size_t_interval(size_t min, size_t max);
-
+extern size_t Frama_C_size_t_interval(size_t min, size_t max)
+ __attribute__((FC_BUILTIN));
/*@ requires finite: \is_finite(min) && \is_finite(max);
requires order: min <= max;
@@ -154,7 +160,8 @@ extern size_t Frama_C_size_t_interval(size_t min, size_t max);
assigns Frama_C_entropy_source \from Frama_C_entropy_source;
ensures result_bounded: \is_finite(\result) && min <= \result <= max;
*/
-extern float Frama_C_float_interval(float min, float max);
+extern float Frama_C_float_interval(float min, float max)
+ __attribute__((FC_BUILTIN));
/*@ requires finite: \is_finite(min) && \is_finite(max);
requires order: min <= max;
@@ -162,7 +169,8 @@ extern float Frama_C_float_interval(float min, float max);
assigns Frama_C_entropy_source \from Frama_C_entropy_source;
ensures result_bounded: \is_finite(\result) && min <= \result <= max;
*/
-extern double Frama_C_double_interval(double min, double max);
+extern double Frama_C_double_interval(double min, double max)
+ __attribute__((FC_BUILTIN));
/*@ requires finite: \is_finite(min) && \is_finite(max);
requires order: min <= max;
@@ -170,32 +178,39 @@ extern double Frama_C_double_interval(double min, double max);
assigns Frama_C_entropy_source \from Frama_C_entropy_source;
ensures result_bounded: \is_finite(\result) && min <= \result <= max;
*/
-extern double Frama_C_real_interval_as_double(double min, double max);
+extern double Frama_C_real_interval_as_double(double min, double max)
+ __attribute__((FC_BUILTIN));
/*@ // Signals an error;
terminates \false;
assigns \nothing;
ensures never_terminates: \false;
*/
-extern void Frama_C_abort(void) __attribute__ ((__noreturn__));
+extern void Frama_C_abort(void) __attribute__((__noreturn__))
+__attribute__((FC_BUILTIN));
/*@ assigns \result \from p; */
-extern size_t Frama_C_offset(const void* p);
+extern size_t Frama_C_offset(const void *p) __attribute__((FC_BUILTIN));
-extern void *Frama_C_malloc_fresh(size_t size);
+extern void *Frama_C_malloc_fresh(size_t size) __attribute__((FC_BUILTIN));
//@ assigns \result \from i;
-extern long long Frama_C_abstract_cardinal(long long i);
+extern long long Frama_C_abstract_cardinal(long long i)
+ __attribute__((FC_BUILTIN));
+
//@ assigns \result \from i;
-extern long long Frama_C_abstract_max(long long i);
+extern long long Frama_C_abstract_max(long long i) __attribute__((FC_BUILTIN));
+
//@ assigns \result \from i;
-extern long long Frama_C_abstract_min(long long i);
+extern long long Frama_C_abstract_min(long long i) __attribute__((FC_BUILTIN));
//@ assigns \nothing;
-extern void Frama_C_watch_value(void *p, size_t size, int i, int n);
+extern void Frama_C_watch_value(void *p, size_t size, int i, int n)
+ __attribute__((FC_BUILTIN));
//@ assigns \nothing;
-extern void Frama_C_watch_cardinal(void *p, size_t size, int i, int n);
+extern void Frama_C_watch_cardinal(void *p, size_t size, int i, int n)
+ __attribute__((FC_BUILTIN));
__END_DECLS
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 6d5c0ae28e11386f874059099f72e95d7aacf487..13006c859426f3ebde563fd698077ba99ec641b1 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -4963,6 +4963,13 @@ and makeVarSizeVarInfo ghost (ldecl : location)
~isglobal:false
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. *)
+ let spec_res = match spec_res with
+ | (t, sto , inline , attrs) when ghost ->
+ (t, sto , inline , ("ghost", []) :: attrs)
+ | normal -> normal
+ in
makeVarInfoCabs ~ghost ~isformal:false
~isglobal:false
ldecl spec_res (n,ndt',a), se, len, true
diff --git a/src/kernel_internals/typing/ghost_accesses.ml b/src/kernel_internals/typing/ghost_accesses.ml
index a123a753dd6b66055de9eabb656c8bd4ff07472c..72ea15e54e5acf994e835c62e6303589397d6f31 100644
--- a/src/kernel_internals/typing/ghost_accesses.ml
+++ b/src/kernel_internals/typing/ghost_accesses.ml
@@ -172,21 +172,22 @@ class visitor = object(self)
if not (isGhostType (typeOfLval lv)) then
Error.assigns_non_ghost_lvalue ~current:true lv
in
- let call_varinfo = function
- | { enode = Lval ( (Var vi), NoOffset ) } -> Some vi
- | _ -> None
+ let is_builtin vi =
+ Ast_info.is_frama_c_builtin vi.vname ||
+ Cil_builtins.is_builtin vi
in
- let is_ghost vi = vi.vghost || Ast_info.is_frama_c_builtin vi.vname in
let failed = match i with
| Call(_, fexp, _, _) ->
- begin match call_varinfo fexp with
- | Some fct when not (is_ghost fct) ->
+ begin match Kernel_function.(Option.map get_vi @@ get_called fexp) with
+ | Some fct
+ when not (is_builtin fct) && not fct.vghost ->
Error.non_ghost_function_call_in_ghost ~current:true () ; true
| None ->
Error.function_pointer_call ~current:true () ; true
| _ -> false
end
- | Local_init(_, ConsInit(fct, _, _), _) when not (is_ghost fct) ->
+ | Local_init(_, ConsInit(fct, _, _), _)
+ when not (is_builtin fct) && not fct.vghost ->
Error.non_ghost_function_call_in_ghost ~current:true () ; true
| _ -> false
in
@@ -197,9 +198,13 @@ class visitor = object(self)
error_if_not_writable lv ;
match i with
| Call(_, fexp, _, _) ->
- error_if_incompatible lv (getReturnType (typeOf fexp)) fexp
+ let vi =
+ Kernel_function.(get_vi @@ Option.get @@ get_called fexp) in
+ if not (is_builtin vi) then
+ error_if_incompatible lv (getReturnType (typeOf fexp)) fexp
| Local_init(_, ConsInit(fct, _, _), _) ->
- error_if_incompatible lv (getReturnType fct.vtype) (evar fct)
+ if not (is_builtin fct) then
+ error_if_incompatible lv (getReturnType fct.vtype) (evar fct)
| _ -> ()
end
(* Note that we do not check "assigns" for a ghost function call since
diff --git a/src/plugins/aorai/tests/ya/oracle/serial.res.oracle b/src/plugins/aorai/tests/ya/oracle/serial.res.oracle
index fc0a491dcf7bcadaa3893e54c598d9e997b3bc53..f6cbbacc42cbecac9183de261ba17490eddb4cf3 100644
--- a/src/plugins/aorai/tests/ya/oracle/serial.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/serial.res.oracle
@@ -291,7 +291,6 @@
----------------------------------------------------------------------------
[kernel] Parsing TMPDIR/aorai_serial_0.i (no preprocessing)
/* Generated by Frama-C */
-typedef unsigned long size_t;
enum aorai_States {
Complete = 0,
DataReq1 = 1,
@@ -332,196 +331,13 @@ enum aorai_OpStatusList {
void Frama_C_show_aorai_state(...); */
extern int volatile Frama_C_entropy_source __attribute__((__unused__));
-/*@ requires valid_p: \valid(p + (0 .. l - 1));
- ensures initialization: \initialized(\old(p) + (0 .. \old(l) - 1));
- assigns *(p + (0 .. l - 1)), Frama_C_entropy_source;
- assigns *(p + (0 .. l - 1)) \from Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-extern void Frama_C_make_unknown(char *p, size_t l);
-
-/*@ ensures result_a_or_b: \result ≡ \old(a) ∨ \result ≡ \old(b);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from a, b, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-extern int Frama_C_nondet(int a, int b);
-
-/*@ ensures result_a_or_b: \result ≡ \old(a) ∨ \result ≡ \old(b);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from a, b, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-extern void *Frama_C_nondet_ptr(void *a, void *b);
-
-/*@ requires order: min ≤ max;
- ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from min, max, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-extern int Frama_C_interval(int min, int max);
-
-/*@ requires order: min ≤ max;
- ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from min, max, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-extern int Frama_C_interval_split(int min, int max);
-
-/*@ requires order: min ≤ max;
- ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from min, max, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-extern unsigned char Frama_C_unsigned_char_interval(unsigned char min,
- unsigned char max);
-
-/*@ requires order: min ≤ max;
- ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from min, max, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-extern char Frama_C_char_interval(char min, char max);
-
-/*@ requires order: min ≤ max;
- ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from min, max, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-extern unsigned short Frama_C_unsigned_short_interval(unsigned short min,
- unsigned short max);
-
-/*@ requires order: min ≤ max;
- ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from min, max, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-extern short Frama_C_short_interval(short min, short max);
-
-/*@ requires order: min ≤ max;
- ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from min, max, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-extern unsigned int Frama_C_unsigned_int_interval(unsigned int min,
- unsigned int max);
-
/*@ requires order: min ≤ max;
ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
assigns \result, Frama_C_entropy_source;
assigns \result \from min, max, Frama_C_entropy_source;
assigns Frama_C_entropy_source \from Frama_C_entropy_source;
*/
-extern int Frama_C_int_interval(int min, int max);
-
-/*@ requires order: min ≤ max;
- ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from min, max, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-extern unsigned long Frama_C_unsigned_long_interval(unsigned long min,
- unsigned long max);
-
-/*@ requires order: min ≤ max;
- ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from min, max, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-extern long Frama_C_long_interval(long min, long max);
-
-/*@ requires order: min ≤ max;
- ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from min, max, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-extern unsigned long long Frama_C_unsigned_long_long_interval(unsigned long long min,
- unsigned long long max);
-
-/*@ requires order: min ≤ max;
- ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from min, max, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-extern long long Frama_C_long_long_interval(long long min, long long max);
-
-/*@ requires order: min ≤ max;
- ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from min, max, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-extern size_t Frama_C_size_t_interval(size_t min, size_t max);
-
-/*@ requires finite: \is_finite(min) ∧ \is_finite(max);
- requires order: min ≤ max;
- ensures
- result_bounded:
- \is_finite(\result) ∧ \old(min) ≤ \result ≤ \old(max);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from min, max, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-extern float Frama_C_float_interval(float min, float max);
-
-/*@ requires finite: \is_finite(min) ∧ \is_finite(max);
- requires order: min ≤ max;
- ensures
- result_bounded:
- \is_finite(\result) ∧ \old(min) ≤ \result ≤ \old(max);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from min, max, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-extern double Frama_C_double_interval(double min, double max);
-
-/*@ requires finite: \is_finite(min) ∧ \is_finite(max);
- requires order: min ≤ max;
- ensures
- result_bounded:
- \is_finite(\result) ∧ \old(min) ≤ \result ≤ \old(max);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from min, max, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-extern double Frama_C_real_interval_as_double(double min, double max);
-
-/*@ terminates \false;
- ensures never_terminates: \false;
- assigns \nothing; */
-extern __attribute__((__noreturn__)) void Frama_C_abort(void);
-
-/*@ assigns \result;
- assigns \result \from p; */
-extern size_t Frama_C_offset(void const *p);
-
-/*@ assigns \result;
- assigns \result \from i; */
-extern long long Frama_C_abstract_cardinal(long long i);
-
-/*@ assigns \result;
- assigns \result \from i; */
-extern long long Frama_C_abstract_max(long long i);
-
-/*@ assigns \result;
- assigns \result \from i; */
-extern long long Frama_C_abstract_min(long long i);
-
-/*@ assigns \nothing; */
-extern void Frama_C_watch_value(void *p, size_t size, int i, int n);
-
-/*@ assigns \nothing; */
-extern void Frama_C_watch_cardinal(void *p, size_t size, int i, int n);
+extern __attribute__((__FC_BUILTIN__)) int Frama_C_interval(int min, int max);
int volatile indefinitely;
int buffer[5];
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle
index a171b4de92e5e8d97fb60209feb3f84a58c6fe4a..80915856615d80692afbea34a939455e0bb02bf8 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing serial.c (with preprocessing)
[kernel] Parsing TMPDIR/aorai_serial_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
-[kernel:annot:missing-spec] TMPDIR/aorai_serial_0_prove.i:1456: Warning:
+[kernel:annot:missing-spec] TMPDIR/aorai_serial_0_prove.i:1273: Warning:
Neither code nor specification for function Frama_C_show_aorai_state, generating default assigns from the prototype
diff --git a/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif b/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
index 226d230c654e28da68998015f8a04d48db53ab90..974b7a37e8fca83ef3f808540f6c5acec657b73b 100644
--- a/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
+++ b/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
@@ -1159,9 +1159,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 180,
+ "startLine": 189,
"startColumn": 12,
- "endLine": 180,
+ "endLine": 189,
"endColumn": 25,
"byteLength": 13
}
@@ -1182,9 +1182,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 178,
+ "startLine": 187,
"startColumn": 28,
- "endLine": 178,
+ "endLine": 187,
"endColumn": 34,
"byteLength": 6
}
@@ -1205,9 +1205,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 180,
+ "startLine": 189,
"startColumn": 12,
- "endLine": 180,
+ "endLine": 189,
"endColumn": 25,
"byteLength": 13
}
@@ -1228,9 +1228,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 176,
+ "startLine": 185,
"startColumn": 13,
- "endLine": 176,
+ "endLine": 185,
"endColumn": 19,
"byteLength": 6
}
@@ -1254,9 +1254,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 188,
+ "startLine": 198,
"startColumn": 17,
- "endLine": 188,
+ "endLine": 198,
"endColumn": 42,
"byteLength": 25
}
@@ -1279,9 +1279,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 188,
+ "startLine": 198,
"startColumn": 17,
- "endLine": 188,
+ "endLine": 198,
"endColumn": 42,
"byteLength": 25
}
@@ -1305,9 +1305,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 187,
+ "startLine": 197,
"startColumn": 12,
- "endLine": 187,
+ "endLine": 197,
"endColumn": 19,
"byteLength": 7
}
@@ -1330,9 +1330,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 190,
+ "startLine": 202,
"startColumn": 17,
- "endLine": 190,
+ "endLine": 202,
"endColumn": 37,
"byteLength": 20
}
@@ -1355,9 +1355,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 190,
+ "startLine": 202,
"startColumn": 17,
- "endLine": 190,
+ "endLine": 202,
"endColumn": 37,
"byteLength": 20
}
@@ -1381,9 +1381,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 189,
+ "startLine": 201,
"startColumn": 12,
- "endLine": 189,
+ "endLine": 201,
"endColumn": 19,
"byteLength": 7
}
@@ -1406,9 +1406,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 192,
+ "startLine": 205,
"startColumn": 17,
- "endLine": 192,
+ "endLine": 205,
"endColumn": 37,
"byteLength": 20
}
@@ -1431,9 +1431,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 192,
+ "startLine": 205,
"startColumn": 17,
- "endLine": 192,
+ "endLine": 205,
"endColumn": 37,
"byteLength": 20
}
@@ -1457,9 +1457,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 191,
+ "startLine": 204,
"startColumn": 12,
- "endLine": 191,
+ "endLine": 204,
"endColumn": 19,
"byteLength": 7
}
@@ -1482,9 +1482,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 79,
+ "startLine": 80,
"startColumn": 12,
- "endLine": 79,
+ "endLine": 80,
"endColumn": 33,
"byteLength": 21
}
@@ -1505,9 +1505,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 74,
+ "startLine": 75,
"startColumn": 20,
- "endLine": 74,
+ "endLine": 75,
"endColumn": 30,
"byteLength": 10
}
@@ -1528,9 +1528,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 77,
+ "startLine": 78,
"startColumn": 28,
- "endLine": 77,
+ "endLine": 78,
"endColumn": 49,
"byteLength": 21
}
@@ -1553,9 +1553,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 75,
+ "startLine": 76,
"startColumn": 12,
- "endLine": 75,
+ "endLine": 76,
"endColumn": 19,
"byteLength": 7
}
@@ -1579,9 +1579,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 75,
+ "startLine": 76,
"startColumn": 12,
- "endLine": 75,
+ "endLine": 76,
"endColumn": 19,
"byteLength": 7
}
@@ -1605,9 +1605,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 76,
+ "startLine": 77,
"startColumn": 12,
- "endLine": 76,
+ "endLine": 77,
"endColumn": 34,
"byteLength": 22
}
@@ -1630,9 +1630,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 165,
+ "startLine": 172,
"startColumn": 14,
- "endLine": 165,
+ "endLine": 172,
"endColumn": 37,
"byteLength": 23
}
@@ -1653,9 +1653,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 159,
+ "startLine": 166,
"startColumn": 21,
- "endLine": 159,
+ "endLine": 166,
"endColumn": 55,
"byteLength": 34
}
@@ -1676,9 +1676,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 160,
+ "startLine": 167,
"startColumn": 20,
- "endLine": 160,
+ "endLine": 167,
"endColumn": 30,
"byteLength": 10
}
@@ -1699,9 +1699,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 163,
+ "startLine": 170,
"startColumn": 28,
- "endLine": 163,
+ "endLine": 170,
"endColumn": 72,
"byteLength": 44
}
@@ -1724,9 +1724,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 161,
+ "startLine": 168,
"startColumn": 12,
- "endLine": 161,
+ "endLine": 168,
"endColumn": 19,
"byteLength": 7
}
@@ -1750,9 +1750,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 161,
+ "startLine": 168,
"startColumn": 12,
- "endLine": 161,
+ "endLine": 168,
"endColumn": 19,
"byteLength": 7
}
@@ -1776,9 +1776,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 162,
+ "startLine": 169,
"startColumn": 12,
- "endLine": 162,
+ "endLine": 169,
"endColumn": 34,
"byteLength": 22
}
@@ -1801,9 +1801,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 157,
+ "startLine": 163,
"startColumn": 13,
- "endLine": 157,
+ "endLine": 163,
"endColumn": 35,
"byteLength": 22
}
@@ -1824,9 +1824,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 151,
+ "startLine": 157,
"startColumn": 21,
- "endLine": 151,
+ "endLine": 157,
"endColumn": 55,
"byteLength": 34
}
@@ -1847,9 +1847,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 152,
+ "startLine": 158,
"startColumn": 20,
- "endLine": 152,
+ "endLine": 158,
"endColumn": 30,
"byteLength": 10
}
@@ -1870,9 +1870,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 155,
+ "startLine": 161,
"startColumn": 28,
- "endLine": 155,
+ "endLine": 161,
"endColumn": 72,
"byteLength": 44
}
@@ -1895,9 +1895,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 153,
+ "startLine": 159,
"startColumn": 12,
- "endLine": 153,
+ "endLine": 159,
"endColumn": 19,
"byteLength": 7
}
@@ -1921,9 +1921,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 153,
+ "startLine": 159,
"startColumn": 12,
- "endLine": 153,
+ "endLine": 159,
"endColumn": 19,
"byteLength": 7
}
@@ -1947,9 +1947,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 154,
+ "startLine": 160,
"startColumn": 12,
- "endLine": 154,
+ "endLine": 160,
"endColumn": 34,
"byteLength": 22
}
@@ -1972,9 +1972,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 108,
+ "startLine": 114,
"startColumn": 11,
- "endLine": 108,
+ "endLine": 114,
"endColumn": 31,
"byteLength": 20
}
@@ -1995,9 +1995,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 103,
+ "startLine": 109,
"startColumn": 20,
- "endLine": 103,
+ "endLine": 109,
"endColumn": 30,
"byteLength": 10
}
@@ -2018,9 +2018,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 106,
+ "startLine": 112,
"startColumn": 28,
- "endLine": 106,
+ "endLine": 112,
"endColumn": 49,
"byteLength": 21
}
@@ -2043,9 +2043,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 104,
+ "startLine": 110,
"startColumn": 12,
- "endLine": 104,
+ "endLine": 110,
"endColumn": 19,
"byteLength": 7
}
@@ -2069,9 +2069,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 104,
+ "startLine": 110,
"startColumn": 12,
- "endLine": 104,
+ "endLine": 110,
"endColumn": 19,
"byteLength": 7
}
@@ -2095,9 +2095,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 105,
+ "startLine": 111,
"startColumn": 12,
- "endLine": 105,
+ "endLine": 111,
"endColumn": 34,
"byteLength": 22
}
@@ -2416,9 +2416,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 124,
+ "startLine": 130,
"startColumn": 12,
- "endLine": 124,
+ "endLine": 130,
"endColumn": 33,
"byteLength": 21
}
@@ -2439,9 +2439,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 119,
+ "startLine": 125,
"startColumn": 20,
- "endLine": 119,
+ "endLine": 125,
"endColumn": 30,
"byteLength": 10
}
@@ -2462,9 +2462,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 122,
+ "startLine": 128,
"startColumn": 28,
- "endLine": 122,
+ "endLine": 128,
"endColumn": 49,
"byteLength": 21
}
@@ -2487,9 +2487,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 120,
+ "startLine": 126,
"startColumn": 12,
- "endLine": 120,
+ "endLine": 126,
"endColumn": 19,
"byteLength": 7
}
@@ -2513,9 +2513,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 120,
+ "startLine": 126,
"startColumn": 12,
- "endLine": 120,
+ "endLine": 126,
"endColumn": 19,
"byteLength": 7
}
@@ -2539,9 +2539,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 121,
+ "startLine": 127,
"startColumn": 12,
- "endLine": 121,
+ "endLine": 127,
"endColumn": 34,
"byteLength": 22
}
@@ -2565,9 +2565,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 140,
+ "startLine": 146,
"startColumn": 17,
- "endLine": 140,
+ "endLine": 146,
"endColumn": 43,
"byteLength": 26
}
@@ -2588,9 +2588,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 135,
+ "startLine": 141,
"startColumn": 20,
- "endLine": 135,
+ "endLine": 141,
"endColumn": 30,
"byteLength": 10
}
@@ -2611,9 +2611,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 138,
+ "startLine": 144,
"startColumn": 28,
- "endLine": 138,
+ "endLine": 144,
"endColumn": 49,
"byteLength": 21
}
@@ -2636,9 +2636,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 136,
+ "startLine": 142,
"startColumn": 12,
- "endLine": 136,
+ "endLine": 142,
"endColumn": 19,
"byteLength": 7
}
@@ -2662,9 +2662,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 136,
+ "startLine": 142,
"startColumn": 12,
- "endLine": 136,
+ "endLine": 142,
"endColumn": 19,
"byteLength": 7
}
@@ -2688,9 +2688,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 137,
+ "startLine": 143,
"startColumn": 12,
- "endLine": 137,
+ "endLine": 143,
"endColumn": 34,
"byteLength": 22
}
@@ -3109,9 +3109,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 183,
+ "startLine": 193,
"startColumn": 14,
- "endLine": 183,
+ "endLine": 193,
"endColumn": 28,
"byteLength": 14
}
@@ -3132,9 +3132,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 183,
+ "startLine": 193,
"startColumn": 14,
- "endLine": 183,
+ "endLine": 193,
"endColumn": 28,
"byteLength": 14
}
@@ -3158,9 +3158,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 182,
+ "startLine": 192,
"startColumn": 12,
- "endLine": 182,
+ "endLine": 192,
"endColumn": 19,
"byteLength": 7
}
@@ -3184,9 +3184,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 173,
+ "startLine": 181,
"startColumn": 14,
- "endLine": 173,
+ "endLine": 181,
"endColumn": 45,
"byteLength": 31
}
@@ -3207,9 +3207,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 167,
+ "startLine": 175,
"startColumn": 21,
- "endLine": 167,
+ "endLine": 175,
"endColumn": 55,
"byteLength": 34
}
@@ -3230,9 +3230,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 168,
+ "startLine": 176,
"startColumn": 20,
- "endLine": 168,
+ "endLine": 176,
"endColumn": 30,
"byteLength": 10
}
@@ -3253,9 +3253,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 171,
+ "startLine": 179,
"startColumn": 28,
- "endLine": 171,
+ "endLine": 179,
"endColumn": 72,
"byteLength": 44
}
@@ -3279,9 +3279,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 169,
+ "startLine": 177,
"startColumn": 12,
- "endLine": 169,
+ "endLine": 177,
"endColumn": 19,
"byteLength": 7
}
@@ -3305,9 +3305,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 169,
+ "startLine": 177,
"startColumn": 12,
- "endLine": 169,
+ "endLine": 177,
"endColumn": 19,
"byteLength": 7
}
@@ -3331,9 +3331,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 170,
+ "startLine": 178,
"startColumn": 12,
- "endLine": 170,
+ "endLine": 178,
"endColumn": 34,
"byteLength": 22
}
@@ -3356,9 +3356,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 93,
+ "startLine": 97,
"startColumn": 13,
- "endLine": 93,
+ "endLine": 97,
"endColumn": 35,
"byteLength": 22
}
@@ -3379,9 +3379,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 88,
+ "startLine": 92,
"startColumn": 20,
- "endLine": 88,
+ "endLine": 92,
"endColumn": 30,
"byteLength": 10
}
@@ -3402,9 +3402,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 91,
+ "startLine": 95,
"startColumn": 28,
- "endLine": 91,
+ "endLine": 95,
"endColumn": 49,
"byteLength": 21
}
@@ -3427,9 +3427,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 89,
+ "startLine": 93,
"startColumn": 12,
- "endLine": 89,
+ "endLine": 93,
"endColumn": 19,
"byteLength": 7
}
@@ -3453,9 +3453,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 89,
+ "startLine": 93,
"startColumn": 12,
- "endLine": 89,
+ "endLine": 93,
"endColumn": 19,
"byteLength": 7
}
@@ -3479,9 +3479,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 90,
+ "startLine": 94,
"startColumn": 12,
- "endLine": 90,
+ "endLine": 94,
"endColumn": 34,
"byteLength": 22
}
@@ -3504,9 +3504,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 148,
+ "startLine": 154,
"startColumn": 14,
- "endLine": 148,
+ "endLine": 154,
"endColumn": 37,
"byteLength": 23
}
@@ -3527,9 +3527,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 143,
+ "startLine": 149,
"startColumn": 20,
- "endLine": 143,
+ "endLine": 149,
"endColumn": 30,
"byteLength": 10
}
@@ -3550,9 +3550,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 146,
+ "startLine": 152,
"startColumn": 28,
- "endLine": 146,
+ "endLine": 152,
"endColumn": 49,
"byteLength": 21
}
@@ -3575,9 +3575,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 144,
+ "startLine": 150,
"startColumn": 12,
- "endLine": 144,
+ "endLine": 150,
"endColumn": 19,
"byteLength": 7
}
@@ -3601,9 +3601,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 144,
+ "startLine": 150,
"startColumn": 12,
- "endLine": 144,
+ "endLine": 150,
"endColumn": 19,
"byteLength": 7
}
@@ -3627,9 +3627,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 145,
+ "startLine": 151,
"startColumn": 12,
- "endLine": 145,
+ "endLine": 151,
"endColumn": 34,
"byteLength": 22
}
@@ -3803,9 +3803,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 101,
+ "startLine": 105,
"startColumn": 20,
- "endLine": 101,
+ "endLine": 105,
"endColumn": 49,
"byteLength": 29
}
@@ -3826,9 +3826,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 96,
+ "startLine": 100,
"startColumn": 20,
- "endLine": 96,
+ "endLine": 100,
"endColumn": 30,
"byteLength": 10
}
@@ -3849,9 +3849,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 99,
+ "startLine": 103,
"startColumn": 28,
- "endLine": 99,
+ "endLine": 103,
"endColumn": 49,
"byteLength": 21
}
@@ -3875,9 +3875,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 97,
+ "startLine": 101,
"startColumn": 12,
- "endLine": 97,
+ "endLine": 101,
"endColumn": 19,
"byteLength": 7
}
@@ -3901,9 +3901,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 97,
+ "startLine": 101,
"startColumn": 12,
- "endLine": 97,
+ "endLine": 101,
"endColumn": 19,
"byteLength": 7
}
@@ -3927,9 +3927,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 98,
+ "startLine": 102,
"startColumn": 12,
- "endLine": 98,
+ "endLine": 102,
"endColumn": 34,
"byteLength": 22
}
@@ -3953,9 +3953,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 116,
+ "startLine": 121,
"startColumn": 21,
- "endLine": 116,
+ "endLine": 121,
"endColumn": 51,
"byteLength": 30
}
@@ -3976,9 +3976,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 111,
+ "startLine": 116,
"startColumn": 20,
- "endLine": 111,
+ "endLine": 116,
"endColumn": 30,
"byteLength": 10
}
@@ -3999,9 +3999,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 114,
+ "startLine": 119,
"startColumn": 28,
- "endLine": 114,
+ "endLine": 119,
"endColumn": 49,
"byteLength": 21
}
@@ -4025,9 +4025,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 112,
+ "startLine": 117,
"startColumn": 12,
- "endLine": 112,
+ "endLine": 117,
"endColumn": 19,
"byteLength": 7
}
@@ -4051,9 +4051,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 112,
+ "startLine": 117,
"startColumn": 12,
- "endLine": 112,
+ "endLine": 117,
"endColumn": 19,
"byteLength": 7
}
@@ -4077,9 +4077,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 113,
+ "startLine": 118,
"startColumn": 12,
- "endLine": 113,
+ "endLine": 118,
"endColumn": 34,
"byteLength": 22
}
@@ -4103,9 +4103,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 132,
+ "startLine": 138,
"startColumn": 26,
- "endLine": 132,
+ "endLine": 138,
"endColumn": 61,
"byteLength": 35
}
@@ -4126,9 +4126,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 127,
+ "startLine": 133,
"startColumn": 20,
- "endLine": 127,
+ "endLine": 133,
"endColumn": 30,
"byteLength": 10
}
@@ -4149,9 +4149,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 130,
+ "startLine": 136,
"startColumn": 28,
- "endLine": 130,
+ "endLine": 136,
"endColumn": 49,
"byteLength": 21
}
@@ -4175,9 +4175,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 128,
+ "startLine": 134,
"startColumn": 12,
- "endLine": 128,
+ "endLine": 134,
"endColumn": 19,
"byteLength": 7
}
@@ -4201,9 +4201,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 128,
+ "startLine": 134,
"startColumn": 12,
- "endLine": 128,
+ "endLine": 134,
"endColumn": 19,
"byteLength": 7
}
@@ -4227,9 +4227,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 129,
+ "startLine": 135,
"startColumn": 12,
- "endLine": 129,
+ "endLine": 135,
"endColumn": 34,
"byteLength": 22
}
@@ -4253,9 +4253,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 86,
+ "startLine": 88,
"startColumn": 22,
- "endLine": 86,
+ "endLine": 88,
"endColumn": 53,
"byteLength": 31
}
@@ -4276,9 +4276,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 81,
+ "startLine": 83,
"startColumn": 20,
- "endLine": 81,
+ "endLine": 83,
"endColumn": 30,
"byteLength": 10
}
@@ -4299,9 +4299,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 84,
+ "startLine": 86,
"startColumn": 28,
- "endLine": 84,
+ "endLine": 86,
"endColumn": 49,
"byteLength": 21
}
@@ -4325,9 +4325,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 82,
+ "startLine": 84,
"startColumn": 12,
- "endLine": 82,
+ "endLine": 84,
"endColumn": 19,
"byteLength": 7
}
@@ -4351,9 +4351,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 82,
+ "startLine": 84,
"startColumn": 12,
- "endLine": 82,
+ "endLine": 84,
"endColumn": 19,
"byteLength": 7
}
@@ -4377,9 +4377,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 83,
+ "startLine": 85,
"startColumn": 12,
- "endLine": 83,
+ "endLine": 85,
"endColumn": 34,
"byteLength": 22
}
@@ -4402,9 +4402,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 198,
+ "startLine": 212,
"startColumn": 12,
- "endLine": 198,
+ "endLine": 212,
"endColumn": 34,
"byteLength": 22
}
@@ -4427,9 +4427,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 198,
+ "startLine": 212,
"startColumn": 12,
- "endLine": 198,
+ "endLine": 212,
"endColumn": 34,
"byteLength": 22
}
@@ -4452,9 +4452,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 195,
+ "startLine": 208,
"startColumn": 12,
- "endLine": 195,
+ "endLine": 208,
"endColumn": 31,
"byteLength": 19
}
@@ -4477,9 +4477,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 195,
+ "startLine": 208,
"startColumn": 12,
- "endLine": 195,
+ "endLine": 208,
"endColumn": 31,
"byteLength": 19
}
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle
index faadd1df8084289a61a9d27e3c3bfd6d055fb10a..afe53a3b1ad910ea7ce6fa3ab1dff98598de0132 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle
@@ -1,6 +1,8 @@
# frama-c -wp [...]
[kernel] Parsing string_c.c (with preprocessing)
[wp] Running WP plugin...
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/string.c:348: Warning:
+ Neither code nor specification for function Frama_C_malloc_fresh, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
Goal Post-condition 'copied_contents' in 'memcpy':
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/string_c.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/string_c.res.oracle
index 7318a8dbf7a2a15ca46a09755a622c59dca99778..8d9d581ae5b07bb009c988c011c170b588b15664 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/string_c.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/string_c.res.oracle
@@ -1,6 +1,8 @@
# frama-c -wp -wp-timeout 120 -wp-steps 2500 [...]
[kernel] Parsing string_c.c (with preprocessing)
[wp] Running WP plugin...
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/string.c:348: Warning:
+ Neither code nor specification for function Frama_C_malloc_fresh, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] 44 goals scheduled
[wp] [Valid] typed_memcpy_ensures_copied_contents (Alt-Ergo) (Cached)
diff --git a/tests/libc/fc_builtins_in_ghost.c b/tests/libc/fc_builtins_in_ghost.c
new file mode 100644
index 0000000000000000000000000000000000000000..dee454a232e0ce38067c6fb0803d2e207ec8a788
--- /dev/null
+++ b/tests/libc/fc_builtins_in_ghost.c
@@ -0,0 +1,7 @@
+#include "__fc_builtin.h"
+
+int main(void){
+ int i ;
+ //@ ghost Frama_C_show_each(i);
+ //@ ghost int p = Frama_C_int_interval(0, 10);
+}
diff --git a/tests/libc/oracle/argz_c.res.oracle b/tests/libc/oracle/argz_c.res.oracle
index 24cc544eb9131c56c2d2c6ad5cc6bdb61ac14e73..38154c70f762b0b3c003bb9665e58734bb9fe8c1 100644
--- a/tests/libc/oracle/argz_c.res.oracle
+++ b/tests/libc/oracle/argz_c.res.oracle
@@ -52,6 +52,7 @@
\return(argz_replace) == 0, 6 (auto)
\return(argz_next) == 0 (auto)
\return(Frama_C_nondet_ptr) == 0 (auto)
+ \return(Frama_C_malloc_fresh) == 0 (auto)
\return(char_equal_ignore_case) == 0 (auto)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
diff --git a/tests/libc/oracle/coverage.res.oracle b/tests/libc/oracle/coverage.res.oracle
index d09173f9031a2dc4fbd2d38040e0b175e2ae22c4..60b8ff1014ee1cf991dbfaeed1c3cfbc3d38a8c0 100644
--- a/tests/libc/oracle/coverage.res.oracle
+++ b/tests/libc/oracle/coverage.res.oracle
@@ -28,7 +28,7 @@
main: 4 stmts out of 4 (100.0%)
[metrics] Eva coverage statistics
=======================
- Syntactically reachable functions = 2 (out of 116)
+ Syntactically reachable functions = 2 (out of 98)
Semantically reached functions = 2
Coverage estimation = 100.0%
[metrics] Statements analyzed by Eva
diff --git a/tests/libc/oracle/fc_builtins_in_ghost.res.oracle b/tests/libc/oracle/fc_builtins_in_ghost.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..0d46a02edf54ae25582fb34c1838da1810cdabd6
--- /dev/null
+++ b/tests/libc/oracle/fc_builtins_in_ghost.res.oracle
@@ -0,0 +1,20 @@
+[kernel] Parsing fc_builtins_in_ghost.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+
+[eva] fc_builtins_in_ghost.c:5: Frama_C_show_each: ⊥
+[eva] computing for function Frama_C_int_interval <- main.
+ Called from fc_builtins_in_ghost.c:6.
+[eva] using specification for function Frama_C_int_interval
+[eva] fc_builtins_in_ghost.c:6:
+ function Frama_C_int_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_int_interval
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+ Frama_C_entropy_source ∈ [--..--]
+ p ∈ [0..10]
+ __retres ∈ {0}
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 5a35c61690f2dd9a0489f8d22cddd5839c938637..a081af020567740d163a884cea6fb8618fb442ad 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -401,122 +401,19 @@ struct termios {
cc_t c_cc[32] ;
};
int volatile Frama_C_entropy_source __attribute__((__unused__));
-void Frama_C_make_unknown(char *p, size_t l);
+ __attribute__((__FC_BUILTIN__)) void Frama_C_make_unknown(char *p, size_t l);
-int Frama_C_nondet(int a, int b);
+ __attribute__((__FC_BUILTIN__)) int Frama_C_nondet(int a, int b);
-void *Frama_C_nondet_ptr(void *a, void *b);
+ __attribute__((__FC_BUILTIN__)) int Frama_C_interval(int min, int max);
-int Frama_C_interval(int min, int max);
+ __attribute__((__FC_BUILTIN__)) char Frama_C_char_interval(char min,
+ char max);
-/*@ requires order: min ≤ max;
- ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from min, max, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-extern int Frama_C_interval_split(int min, int max);
-
-unsigned char Frama_C_unsigned_char_interval(unsigned char min,
- unsigned char max);
-
-char Frama_C_char_interval(char min, char max);
-
-/*@ requires order: min ≤ max;
- ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from min, max, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-extern unsigned short Frama_C_unsigned_short_interval(unsigned short min,
- unsigned short max);
-
-/*@ requires order: min ≤ max;
- ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from min, max, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-extern short Frama_C_short_interval(short min, short max);
-
-unsigned int Frama_C_unsigned_int_interval(unsigned int min, unsigned int max);
-
-/*@ requires order: min ≤ max;
- ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from min, max, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-extern int Frama_C_int_interval(int min, int max);
-
-unsigned long Frama_C_unsigned_long_interval(unsigned long min,
- unsigned long max);
-
-long Frama_C_long_interval(long min, long max);
-
-/*@ requires order: min ≤ max;
- ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from min, max, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-extern unsigned long long Frama_C_unsigned_long_long_interval(unsigned long long min,
- unsigned long long max);
-
-/*@ requires order: min ≤ max;
- ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from min, max, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-extern long long Frama_C_long_long_interval(long long min, long long max);
+ __attribute__((__FC_BUILTIN__)) unsigned int Frama_C_unsigned_int_interval
+(unsigned int min, unsigned int max);
-/*@ requires order: min ≤ max;
- ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from min, max, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-extern size_t Frama_C_size_t_interval(size_t min, size_t max);
-
-float Frama_C_float_interval(float min, float max);
-
-double Frama_C_double_interval(double min, double max);
-
-/*@ requires finite: \is_finite(min) ∧ \is_finite(max);
- requires order: min ≤ max;
- ensures
- result_bounded:
- \is_finite(\result) ∧ \old(min) ≤ \result ≤ \old(max);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from min, max, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-extern double Frama_C_real_interval_as_double(double min, double max);
-
- __attribute__((__noreturn__)) void Frama_C_abort(void);
-
-/*@ assigns \result;
- assigns \result \from p; */
-extern size_t Frama_C_offset(void const *p);
-
-/*@ assigns \result;
- assigns \result \from i; */
-extern long long Frama_C_abstract_cardinal(long long i);
-
-/*@ assigns \result;
- assigns \result \from i; */
-extern long long Frama_C_abstract_max(long long i);
-
-/*@ assigns \result;
- assigns \result \from i; */
-extern long long Frama_C_abstract_min(long long i);
-
-/*@ assigns \nothing; */
-extern void Frama_C_watch_value(void *p, size_t size, int i, int n);
-
-/*@ assigns \nothing; */
-extern void Frama_C_watch_cardinal(void *p, size_t size, int i, int n);
+ __attribute__((__noreturn__, __FC_BUILTIN__)) void Frama_C_abort(void);
unsigned int volatile __fc_unsigned_int_entropy;
long volatile __fc_long_entropy;
@@ -536,6 +433,7 @@ void Frama_C_update_entropy(void)
assigns *(p + (0 .. l - 1)) \from Frama_C_entropy_source;
assigns Frama_C_entropy_source \from Frama_C_entropy_source;
*/
+ __attribute__((__FC_BUILTIN__)) void Frama_C_make_unknown(char *p, size_t l);
void Frama_C_make_unknown(char *p, size_t l)
{
Frama_C_update_entropy();
@@ -554,6 +452,7 @@ void Frama_C_make_unknown(char *p, size_t l)
assigns \result \from a, b, Frama_C_entropy_source;
assigns Frama_C_entropy_source \from Frama_C_entropy_source;
*/
+ __attribute__((__FC_BUILTIN__)) int Frama_C_nondet(int a, int b);
int Frama_C_nondet(int a, int b)
{
int tmp;
@@ -562,25 +461,13 @@ int Frama_C_nondet(int a, int b)
return tmp;
}
-/*@ ensures result_a_or_b: \result ≡ \old(a) ∨ \result ≡ \old(b);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from a, b, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-void *Frama_C_nondet_ptr(void *a, void *b)
-{
- void *tmp;
- Frama_C_update_entropy();
- if (Frama_C_entropy_source) tmp = a; else tmp = b;
- return tmp;
-}
-
/*@ requires order: min ≤ max;
ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
assigns \result, Frama_C_entropy_source;
assigns \result \from min, max, Frama_C_entropy_source;
assigns Frama_C_entropy_source \from Frama_C_entropy_source;
*/
+ __attribute__((__FC_BUILTIN__)) int Frama_C_interval(int min, int max);
int Frama_C_interval(int min, int max)
{
int r;
@@ -599,6 +486,8 @@ int Frama_C_interval(int min, int max)
assigns \result \from min, max, Frama_C_entropy_source;
assigns Frama_C_entropy_source \from Frama_C_entropy_source;
*/
+ __attribute__((__FC_BUILTIN__)) char Frama_C_char_interval(char min,
+ char max);
char Frama_C_char_interval(char min, char max)
{
char __retres;
@@ -608,62 +497,14 @@ char Frama_C_char_interval(char min, char max)
return __retres;
}
-/*@ requires finite: \is_finite(min) ∧ \is_finite(max);
- requires order: min ≤ max;
- ensures
- result_bounded:
- \is_finite(\result) ∧ \old(min) ≤ \result ≤ \old(max);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from min, max, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-float Frama_C_float_interval(float min, float max)
-{
- float tmp;
- Frama_C_update_entropy();
- if (Frama_C_entropy_source) tmp = min; else tmp = max;
- return tmp;
-}
-
-/*@ requires finite: \is_finite(min) ∧ \is_finite(max);
- requires order: min ≤ max;
- ensures
- result_bounded:
- \is_finite(\result) ∧ \old(min) ≤ \result ≤ \old(max);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from min, max, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-double Frama_C_double_interval(double min, double max)
-{
- double tmp;
- Frama_C_update_entropy();
- if (Frama_C_entropy_source) tmp = min; else tmp = max;
- return tmp;
-}
-
-/*@ requires order: min ≤ max;
- ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from min, max, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-unsigned char Frama_C_unsigned_char_interval(unsigned char min,
- unsigned char max)
-{
- unsigned char __retres;
- int tmp;
- tmp = Frama_C_interval((int)min,(int)max);
- __retres = (unsigned char)tmp;
- return __retres;
-}
-
/*@ requires order: min ≤ max;
ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
assigns \result, Frama_C_entropy_source;
assigns \result \from min, max, Frama_C_entropy_source;
assigns Frama_C_entropy_source \from Frama_C_entropy_source;
*/
+ __attribute__((__FC_BUILTIN__)) unsigned int Frama_C_unsigned_int_interval
+(unsigned int min, unsigned int max);
unsigned int Frama_C_unsigned_int_interval(unsigned int min, unsigned int max)
{
unsigned int r;
@@ -676,49 +517,12 @@ unsigned int Frama_C_unsigned_int_interval(unsigned int min, unsigned int max)
return r;
}
-/*@ requires order: min ≤ max;
- ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from min, max, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-long Frama_C_long_interval(long min, long max)
-{
- long r;
- long aux;
- Frama_C_update_entropy();
- aux = __fc_long_entropy;
- if (aux >= min)
- if (aux <= max) r = aux; else r = min;
- else r = min;
- return r;
-}
-
-/*@ requires order: min ≤ max;
- ensures result_bounded: \old(min) ≤ \result ≤ \old(max);
- assigns \result, Frama_C_entropy_source;
- assigns \result \from min, max, Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
- */
-unsigned long Frama_C_unsigned_long_interval(unsigned long min,
- unsigned long max)
-{
- unsigned long r;
- unsigned long aux;
- Frama_C_update_entropy();
- aux = __fc_unsigned_long_entropy;
- if (aux >= min)
- if (aux <= max) r = aux; else r = min;
- else r = min;
- return r;
-}
-
extern __attribute__((__noreturn__)) void __builtin_abort(void);
/*@ terminates \false;
ensures never_terminates: \false;
assigns \nothing; */
- __attribute__((__noreturn__)) void Frama_C_abort(void);
+ __attribute__((__noreturn__, __FC_BUILTIN__)) void Frama_C_abort(void);
void Frama_C_abort(void)
{
__builtin_abort();
diff --git a/tests/libc/oracle/netdb_c.res.oracle b/tests/libc/oracle/netdb_c.res.oracle
index dd5fb9f0607ec68958b8e2a81e9ba45e0ee0e3fe..3d81a1c5006d30b08dfbb1afd43caec4a9204dfc 100644
--- a/tests/libc/oracle/netdb_c.res.oracle
+++ b/tests/libc/oracle/netdb_c.res.oracle
@@ -52,6 +52,7 @@
\return(gethostbyname) == 0 (auto)
\return(Frama_C_nondet) == 0 (auto)
\return(Frama_C_nondet_ptr) == 0 (auto)
+ \return(Frama_C_malloc_fresh) == 0 (auto)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
diff --git a/tests/syntax/ghost_vla.i b/tests/syntax/ghost_vla.i
new file mode 100644
index 0000000000000000000000000000000000000000..e2fbc9a738198c33b9f84bd47730a7d7d4dacfd1
--- /dev/null
+++ b/tests/syntax/ghost_vla.i
@@ -0,0 +1,9 @@
+int local_vla(int len){
+ //@ ghost int a[len];
+ //@ ghost a[4] = 32;
+ return 42;
+}
+
+void formal_vla(int len) /*@ ghost (int a[len]) */{
+ //@ ghost a[4] = 32;
+}
diff --git a/tests/syntax/oracle/ghost_vla.res.oracle b/tests/syntax/oracle/ghost_vla.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..fba7be0da522d7865730b903feb102be92a63c80
--- /dev/null
+++ b/tests/syntax/oracle/ghost_vla.res.oracle
@@ -0,0 +1,34 @@
+[kernel] Parsing ghost_vla.i (no preprocessing)
+/* Generated by Frama-C */
+/*@ assigns \nothing;
+ frees p; */
+ __attribute__((__FC_BUILTIN__)) void __fc_vla_free(void *p);
+
+/*@ assigns \result;
+ assigns \result \from \nothing;
+ allocates \result; */
+ __attribute__((__FC_BUILTIN__)) void *__fc_vla_alloc(unsigned int size);
+
+int local_vla(int len)
+{
+ int __retres;
+ /*@ ghost unsigned int __lengthof_a; */
+ /*@ ghost
+ /@ assert alloca_bounds: 0 < sizeof(int \ghost) * len ≤ 4294967295; @/
+ ;
+ __lengthof_a = (unsigned int)len;
+ int \ghost *a = __fc_vla_alloc(sizeof(int \ghost) * __lengthof_a);
+ */
+ /*@ ghost *(a + 4) = 32; */
+ __retres = 42;
+ __fc_vla_free((void *)a);
+ return __retres;
+}
+
+void formal_vla(int len) /*@ ghost (int \ghost a[len]) */
+{
+ /*@ ghost *(a + 4) = 32; */
+ return;
+}
+
+