Skip to content
Snippets Groups Projects
Commit c72da78a authored by Kostyantyn Vorobyov's avatar Kostyantyn Vorobyov
Browse files

Update test case oracles as per Frama-C MR# !1112

parent a843e683
No related branches found
No related tags found
No related merge requests found
[e-acsl] beginning translation. [e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype FRAMAC_SHARE/libc/stdlib.h:277:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown. FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/bts/bts1740.i:12:[value] warning: locals {a} escaping the scope of a block of main through p tests/bts/bts1740.i:12:[value] warning: locals {a} escaping the scope of a block of main through p
......
/* Generated by Frama-C */ /* Generated by Frama-C */
#include "stdlib.h"
int main(void) int main(void)
{ {
int __retres; int __retres;
int *p; int *p;
__e_acsl_memory_init((int *)0,(char ***)0,8UL); __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_store_block((void *)(& p),8UL); __e_acsl_store_block((void *)(& p),(size_t)8);
{ {
int a; int a;
__e_acsl_store_block((void *)(& a),4UL); __e_acsl_store_block((void *)(& a),(size_t)4);
__e_acsl_full_init((void *)(& a)); __e_acsl_full_init((void *)(& a));
a = 0; a = 0;
__e_acsl_full_init((void *)(& p)); __e_acsl_full_init((void *)(& p));
......
[e-acsl] beginning translation. [e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype FRAMAC_SHARE/libc/stdlib.h:277:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown. FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/runtime/bypassed_var.c:16:[value] warning: accessing uninitialized left-value. assert \initialized(&p); tests/runtime/bypassed_var.c:16:[value] warning: accessing uninitialized left-value. assert \initialized(&p);
[e-acsl] beginning translation. [e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype FRAMAC_SHARE/libc/stdlib.h:277:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown. FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/runtime/early_exit.c:14:[value] warning: locals {a} escaping the scope of a block of goto_bts through p tests/runtime/early_exit.c:14:[value] warning: locals {a} escaping the scope of a block of goto_bts through p
......
/* Generated by Frama-C */ /* Generated by Frama-C */
#include "stdlib.h"
int bypassed_var(int i) int bypassed_var(int i)
{ {
int lst[2]; int lst[2];
__e_acsl_store_block((void *)(lst),8UL); __e_acsl_store_block((void *)(lst),(size_t)8);
if (i) goto L; if (i) goto L;
{ {
int *p; int *p;
__e_acsl_store_block((void *)(& p),8UL); __e_acsl_store_block((void *)(& p),(size_t)8);
__e_acsl_full_init((void *)(& p)); __e_acsl_full_init((void *)(& p));
p = (int *)(& lst); p = (int *)(& lst);
L: __e_acsl_store_block_duplicate((void *)(& p),8UL); L: __e_acsl_store_block_duplicate((void *)(& p),(size_t)8);
__e_acsl_full_init((void *)(& p)); __e_acsl_full_init((void *)(& p));
/*@ assert Value: initialisation: \initialized(&p); */ /*@ assert Value: initialisation: \initialized(&p); */
p ++; p ++;
...@@ -60,7 +61,7 @@ int bypassed_var(int i) ...@@ -60,7 +61,7 @@ int bypassed_var(int i)
int main(int argc, char const **argv) int main(int argc, char const **argv)
{ {
int __retres; int __retres;
__e_acsl_memory_init(& argc,(char ***)(& argv),8UL); __e_acsl_memory_init(& argc,(char ***)(& argv),(size_t)8);
bypassed_var(0); bypassed_var(0);
bypassed_var(1); bypassed_var(1);
__retres = 0; __retres = 0;
......
/* Generated by Frama-C */ /* Generated by Frama-C */
#include "stdlib.h"
int goto_bts(void) int goto_bts(void)
{ {
int __retres; int __retres;
int *p; int *p;
__e_acsl_store_block((void *)(& p),8UL); __e_acsl_store_block((void *)(& p),(size_t)8);
{ {
int a; int a;
__e_acsl_store_block((void *)(& a),4UL); __e_acsl_store_block((void *)(& a),(size_t)4);
__e_acsl_full_init((void *)(& a)); __e_acsl_full_init((void *)(& a));
a = 0; a = 0;
__e_acsl_full_init((void *)(& p)); __e_acsl_full_init((void *)(& p));
...@@ -63,27 +64,27 @@ int goto_valid(void) ...@@ -63,27 +64,27 @@ int goto_valid(void)
int *p; int *p;
int *q; int *q;
int *r; int *r;
__e_acsl_store_block((void *)(& r),8UL); __e_acsl_store_block((void *)(& r),(size_t)8);
__e_acsl_store_block((void *)(& q),8UL); __e_acsl_store_block((void *)(& q),(size_t)8);
__e_acsl_store_block((void *)(& p),8UL); __e_acsl_store_block((void *)(& p),(size_t)8);
a = 9; a = 9;
{ {
int a1; int a1;
__e_acsl_store_block((void *)(& a1),4UL); __e_acsl_store_block((void *)(& a1),(size_t)4);
__e_acsl_full_init((void *)(& a1)); __e_acsl_full_init((void *)(& a1));
a1 = 0; a1 = 0;
__e_acsl_full_init((void *)(& p)); __e_acsl_full_init((void *)(& p));
p = & a1; p = & a1;
{ {
int a2; int a2;
__e_acsl_store_block((void *)(& a2),4UL); __e_acsl_store_block((void *)(& a2),(size_t)4);
__e_acsl_full_init((void *)(& a2)); __e_acsl_full_init((void *)(& a2));
a2 = 0; a2 = 0;
__e_acsl_full_init((void *)(& q)); __e_acsl_full_init((void *)(& q));
q = & a2; q = & a2;
{ {
int a3; int a3;
__e_acsl_store_block((void *)(& a3),4UL); __e_acsl_store_block((void *)(& a3),(size_t)4);
__e_acsl_full_init((void *)(& a3)); __e_acsl_full_init((void *)(& a3));
a3 = 0; a3 = 0;
__e_acsl_full_init((void *)(& r)); __e_acsl_full_init((void *)(& r));
...@@ -238,10 +239,10 @@ int switch_valid(void) ...@@ -238,10 +239,10 @@ int switch_valid(void)
int *p; int *p;
int *q; int *q;
int *s; int *s;
__e_acsl_store_block((void *)(& s),8UL); __e_acsl_store_block((void *)(& s),(size_t)8);
__e_acsl_store_block((void *)(& q),8UL); __e_acsl_store_block((void *)(& q),(size_t)8);
__e_acsl_store_block((void *)(& p),8UL); __e_acsl_store_block((void *)(& p),(size_t)8);
__e_acsl_store_block((void *)(& i),4UL); __e_acsl_store_block((void *)(& i),(size_t)4);
__e_acsl_full_init((void *)(& i)); __e_acsl_full_init((void *)(& i));
i = 1; i = 1;
__e_acsl_full_init((void *)(& s)); __e_acsl_full_init((void *)(& s));
...@@ -250,14 +251,14 @@ int switch_valid(void) ...@@ -250,14 +251,14 @@ int switch_valid(void)
default: ; default: ;
{ {
int a1; int a1;
__e_acsl_store_block((void *)(& a1),4UL); __e_acsl_store_block((void *)(& a1),(size_t)4);
__e_acsl_full_init((void *)(& a1)); __e_acsl_full_init((void *)(& a1));
a1 = 0; a1 = 0;
__e_acsl_full_init((void *)(& p)); __e_acsl_full_init((void *)(& p));
p = & a1; p = & a1;
{ {
int a2; int a2;
__e_acsl_store_block((void *)(& a2),4UL); __e_acsl_store_block((void *)(& a2),(size_t)4);
__e_acsl_full_init((void *)(& a2)); __e_acsl_full_init((void *)(& a2));
a2 = 0; a2 = 0;
__e_acsl_full_init((void *)(& q)); __e_acsl_full_init((void *)(& q));
...@@ -397,13 +398,13 @@ int while_valid(void) ...@@ -397,13 +398,13 @@ int while_valid(void)
int *q; int *q;
int *r; int *r;
int i; int i;
__e_acsl_store_block((void *)(& r),8UL); __e_acsl_store_block((void *)(& r),(size_t)8);
__e_acsl_store_block((void *)(& q),8UL); __e_acsl_store_block((void *)(& q),(size_t)8);
__e_acsl_store_block((void *)(& p),8UL); __e_acsl_store_block((void *)(& p),(size_t)8);
i = 5; i = 5;
{ {
int a0; int a0;
__e_acsl_store_block((void *)(& a0),4UL); __e_acsl_store_block((void *)(& a0),(size_t)4);
__e_acsl_full_init((void *)(& a0)); __e_acsl_full_init((void *)(& a0));
a0 = 0; a0 = 0;
__e_acsl_full_init((void *)(& r)); __e_acsl_full_init((void *)(& r));
...@@ -413,14 +414,14 @@ int while_valid(void) ...@@ -413,14 +414,14 @@ int while_valid(void)
if (! i) break; if (! i) break;
{ {
int a1; int a1;
__e_acsl_store_block((void *)(& a1),4UL); __e_acsl_store_block((void *)(& a1),(size_t)4);
__e_acsl_full_init((void *)(& a1)); __e_acsl_full_init((void *)(& a1));
a1 = 0; a1 = 0;
__e_acsl_full_init((void *)(& p)); __e_acsl_full_init((void *)(& p));
p = & a1; p = & a1;
{ {
int a2; int a2;
__e_acsl_store_block((void *)(& a2),4UL); __e_acsl_store_block((void *)(& a2),(size_t)4);
__e_acsl_full_init((void *)(& a2)); __e_acsl_full_init((void *)(& a2));
a2 = 0; a2 = 0;
__e_acsl_full_init((void *)(& q)); __e_acsl_full_init((void *)(& q));
...@@ -555,8 +556,8 @@ void continue_valid(void) ...@@ -555,8 +556,8 @@ void continue_valid(void)
int i; int i;
int *p; int *p;
int *q; int *q;
__e_acsl_store_block((void *)(& q),8UL); __e_acsl_store_block((void *)(& q),(size_t)8);
__e_acsl_store_block((void *)(& p),8UL); __e_acsl_store_block((void *)(& p),(size_t)8);
i = 0; i = 0;
while (1) { while (1) {
int tmp; int tmp;
...@@ -568,7 +569,7 @@ void continue_valid(void) ...@@ -568,7 +569,7 @@ void continue_valid(void)
if (! tmp) break; if (! tmp) break;
{ {
int a1; int a1;
__e_acsl_store_block((void *)(& a1),4UL); __e_acsl_store_block((void *)(& a1),(size_t)4);
/*@ assert ¬\valid(p); */ /*@ assert ¬\valid(p); */
{ {
{ {
...@@ -643,7 +644,7 @@ void continue_valid(void) ...@@ -643,7 +644,7 @@ void continue_valid(void)
} }
{ {
int a2; int a2;
__e_acsl_store_block((void *)(& a2),4UL); __e_acsl_store_block((void *)(& a2),(size_t)4);
__e_acsl_full_init((void *)(& a2)); __e_acsl_full_init((void *)(& a2));
a2 = 1; a2 = 1;
__e_acsl_full_init((void *)(& q)); __e_acsl_full_init((void *)(& q));
...@@ -738,7 +739,7 @@ void continue_valid(void) ...@@ -738,7 +739,7 @@ void continue_valid(void)
int main(int argc, char const **argv) int main(int argc, char const **argv)
{ {
int __retres; int __retres;
__e_acsl_memory_init(& argc,(char ***)(& argv),8UL); __e_acsl_memory_init(& argc,(char ***)(& argv),(size_t)8);
goto_bts(); goto_bts();
goto_valid(); goto_valid();
switch_valid(); switch_valid();
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment