Skip to content
Snippets Groups Projects
Commit 4121ec2f authored by Jan Rochel's avatar Jan Rochel
Browse files

[e-acsl] fix segfault for example

This is not detected by Eva because:
"no assigns clause generated for function length because pointers as arguments is not yet supported"
parent f2318833
No related branches found
No related tags found
No related merge requests found
...@@ -24,6 +24,7 @@ int main(void) { ...@@ -24,6 +24,7 @@ int main(void) {
struct list node1, node2, node3; struct list node1, node2, node3;
node1.next = &node2; node1.next = &node2;
node2.next = &node3; node2.next = &node3;
node3.next = NULL;
struct list *l = &node1; struct list *l = &node1;
/*@ assert length(l) == 3; */; /*@ assert length(l) == 3; */;
} }
[e-acsl] beginning translation. [e-acsl] beginning translation.
[e-acsl] functions_contiki.c:28: Warning: [e-acsl] functions_contiki.c:29: Warning:
no assigns clause generated for function length because pointers as arguments is not yet supported no assigns clause generated for function length because pointers as arguments is not yet supported
[e-acsl] functions_contiki.c:28: Warning: [e-acsl] functions_contiki.c:29: Warning:
no assigns clause generated for function length_aux because pointers as arguments is not yet supported no assigns clause generated for function length_aux because pointers as arguments is not yet supported
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[eva:alarm] functions_contiki.c:18: Warning: [eva:alarm] functions_contiki.c:29: Warning:
accessing uninitialized left-value. assert \initialized(&l->next); function __e_acsl_assert_register_long: precondition data->values == \null ||
\valid(data->values) got status unknown.
[eva:alarm] functions_contiki.c:29: Warning: assertion got status unknown.
...@@ -41,6 +41,8 @@ int main(void) ...@@ -41,6 +41,8 @@ int main(void)
node1.next = & node2; node1.next = & node2;
__e_acsl_initialize((void *)(& node2.next),sizeof(struct list *)); __e_acsl_initialize((void *)(& node2.next),sizeof(struct list *));
node2.next = & node3; node2.next = & node3;
__e_acsl_initialize((void *)(& node3.next),sizeof(struct list *));
node3.next = (struct list *)0;
struct list *l = & node1; struct list *l = & node1;
__e_acsl_store_block((void *)(& l),8UL); __e_acsl_store_block((void *)(& l),8UL);
__e_acsl_full_init((void *)(& l)); __e_acsl_full_init((void *)(& l));
...@@ -57,7 +59,7 @@ int main(void) ...@@ -57,7 +59,7 @@ int main(void)
__gen_e_acsl_assert_data.pred_txt = "length(l) == 3"; __gen_e_acsl_assert_data.pred_txt = "length(l) == 3";
__gen_e_acsl_assert_data.file = "functions_contiki.c"; __gen_e_acsl_assert_data.file = "functions_contiki.c";
__gen_e_acsl_assert_data.fct = "main"; __gen_e_acsl_assert_data.fct = "main";
__gen_e_acsl_assert_data.line = 28; __gen_e_acsl_assert_data.line = 29;
__e_acsl_assert(__gen_e_acsl_length_here_2 == 3L, __e_acsl_assert(__gen_e_acsl_length_here_2 == 3L,
& __gen_e_acsl_assert_data); & __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data); __e_acsl_assert_clean(& __gen_e_acsl_assert_data);
...@@ -90,7 +92,6 @@ long __gen_e_acsl_length_aux_here(struct list *l, unsigned int n) ...@@ -90,7 +92,6 @@ long __gen_e_acsl_length_aux_here(struct list *l, unsigned int n)
long __gen_e_acsl_if; long __gen_e_acsl_if;
if (n < 2147483647U) { if (n < 2147483647U) {
long __gen_e_acsl_length_aux_here_3; long __gen_e_acsl_length_aux_here_3;
/*@ assert Eva: initialization: \initialized(&l->next); */
__gen_e_acsl_length_aux_here_3 = __gen_e_acsl_length_aux_here __gen_e_acsl_length_aux_here_3 = __gen_e_acsl_length_aux_here
(l->next,n + 1U); (l->next,n + 1U);
__gen_e_acsl_if = __gen_e_acsl_length_aux_here_3; __gen_e_acsl_if = __gen_e_acsl_length_aux_here_3;
......
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