Skip to content
Snippets Groups Projects
Commit 45df7ba1 authored by Basile Desloges's avatar Basile Desloges
Browse files

[kernel] Update test oracles

parent 74ce44d0
No related branches found
No related tags found
No related merge requests found
......@@ -68,7 +68,8 @@
"typing:implicit-function-declaration", "typing:implicit-int",
"typing:incompatible-pointer-types",
"typing:incompatible-types-call", "typing:inconsistent-specifier",
"typing:int-conversion", "typing:merge-conversion", "typing:no-proto"
"typing:int-conversion", "typing:merge-conversion",
"typing:no-proto", "unknown-attribute"
],
"disabled": [
"CERT:EXP:10", "acsl-float-compare", "c11", "file:not-found",
......
......@@ -9,7 +9,7 @@
void f(char const * __attribute__((__whatever__)) a,
char * __attribute__((__p__)) b)
{
/*@ assert p((char *)b); */ ;
/*@ assert p(b); */ ;
return;
}
......
[kernel] Parsing array_formals.i (no preprocessing)
[kernel:unknown-attribute] array_formals.i:7: Warning: Unknown attribute: test
/* Generated by Frama-C */
typedef int ( __attribute__((__test__)) arr)[2];
int f(int a[2])
......
[kernel] Parsing attributes-declarations-definitions.c (with preprocessing)
[kernel:unknown-attribute] attributes-declarations-definitions.c:7: Warning:
Unknown attribute: tret1
[kernel:unknown-attribute] attributes-declarations-definitions.c:7: Warning:
Unknown attribute: f1
[kernel:unknown-attribute] attributes-declarations-definitions.c:7: Warning:
Unknown attribute: arg1
[kernel:unknown-attribute] attributes-declarations-definitions.c:10: Warning:
Unknown attribute: tret2
[kernel:unknown-attribute] attributes-declarations-definitions.c:10: Warning:
Unknown attribute: f2
[kernel:unknown-attribute] attributes-declarations-definitions.c:10: Warning:
Unknown attribute: arg2
[kernel:unknown-attribute] attributes-declarations-definitions.c:13: Warning:
Unknown attribute: tret3
[kernel:unknown-attribute] attributes-declarations-definitions.c:13: Warning:
Unknown attribute: arg3
[kernel] attributes-declarations-definitions.c:12: Warning:
found two contracts (old location: attributes-declarations-definitions.c:6). Merging them
[kernel:unknown-attribute] attributes-declarations-definitions.c:21: Warning:
Unknown attribute: tret4
[kernel:unknown-attribute] attributes-declarations-definitions.c:21: Warning:
Unknown attribute: f4
[kernel:unknown-attribute] attributes-declarations-definitions.c:21: Warning:
Unknown attribute: arg4
[kernel] attributes-declarations-definitions.c:21: Warning:
found two contracts (old location: attributes-declarations-definitions.c:13). Merging them
[kernel:unknown-attribute] attributes-declarations-definitions.c:23: Warning:
Unknown attribute: tret5
[kernel:unknown-attribute] attributes-declarations-definitions.c:23: Warning:
Unknown attribute: f5
[kernel:unknown-attribute] attributes-declarations-definitions.c:25: Warning:
Unknown attribute: a1
[kernel:unknown-attribute] attributes-declarations-definitions.c:33: Warning:
Unknown attribute: a2
[kernel:unknown-attribute] attributes-declarations-definitions.c:38: Warning:
Unknown attribute: p1
[kernel:unknown-attribute] attributes-declarations-definitions.c:38: Warning:
Unknown attribute: p2
[kernel:unknown-attribute] attributes-declarations-definitions.c:56: Warning:
Unknown attribute: _n
[kernel:unknown-attribute] attributes-declarations-definitions.c:58: Warning:
Unknown attribute: e_
/* Generated by Frama-C */
typedef int __attribute__((__a1__)) aint;
typedef int __attribute__((__p1__)) * __attribute__((__p2__)) iptr;
......@@ -19,18 +57,14 @@ int __attribute__((__tret5__, __tret4__, __tret3__, __tret2__, __tret1__)) f
int __attribute__((__tret5__, __tret4__, __tret3__, __tret2__, __tret1__)) f
(int const __attribute__((__arg3__)) p3)
{
int __attribute__((__tret5__, __tret4__, __tret3__, __tret2__, __tret1__)) __retres;
__retres = (int __attribute__((__tret3__, __tret2__, __tret1__)))p3;
return __retres;
return p3;
}
aint g(int __attribute__((__a2__)) i3);
aint g(int __attribute__((__a2__)) i3)
{
aint __retres;
__retres = (aint)i3;
return __retres;
return i3;
}
iptr h(iptr volatile ip2);
......
[kernel] Parsing attributes-declarations-definitions.c (with preprocessing)
[kernel:unknown-attribute] attributes-declarations-definitions.c:7: Warning:
Unknown attribute: tret1
[kernel:unknown-attribute] attributes-declarations-definitions.c:7: Warning:
Unknown attribute: f1
[kernel:unknown-attribute] attributes-declarations-definitions.c:7: Warning:
Unknown attribute: arg1
[kernel:unknown-attribute] attributes-declarations-definitions.c:10: Warning:
Unknown attribute: tret2
[kernel:unknown-attribute] attributes-declarations-definitions.c:10: Warning:
Unknown attribute: f2
[kernel:unknown-attribute] attributes-declarations-definitions.c:10: Warning:
Unknown attribute: arg2
[kernel:unknown-attribute] attributes-declarations-definitions.c:13: Warning:
Unknown attribute: tret3
[kernel:unknown-attribute] attributes-declarations-definitions.c:13: Warning:
Unknown attribute: arg3
[kernel] attributes-declarations-definitions.c:12: Warning:
found two contracts (old location: attributes-declarations-definitions.c:6). Merging them
[kernel:unknown-attribute] attributes-declarations-definitions.c:21: Warning:
Unknown attribute: tret4
[kernel:unknown-attribute] attributes-declarations-definitions.c:21: Warning:
Unknown attribute: f4
[kernel:unknown-attribute] attributes-declarations-definitions.c:21: Warning:
Unknown attribute: arg4
[kernel] attributes-declarations-definitions.c:21: Warning:
found two contracts (old location: attributes-declarations-definitions.c:13). Merging them
[kernel:unknown-attribute] attributes-declarations-definitions.c:23: Warning:
Unknown attribute: tret5
[kernel:unknown-attribute] attributes-declarations-definitions.c:23: Warning:
Unknown attribute: f5
[kernel:unknown-attribute] attributes-declarations-definitions.c:25: Warning:
Unknown attribute: a1
[kernel:unknown-attribute] attributes-declarations-definitions.c:33: Warning:
Unknown attribute: a2
[kernel:unknown-attribute] attributes-declarations-definitions.c:38: Warning:
Unknown attribute: p1
[kernel:unknown-attribute] attributes-declarations-definitions.c:38: Warning:
Unknown attribute: p2
[kernel:unknown-attribute] attributes-declarations-definitions.c:56: Warning:
Unknown attribute: _n
[kernel:unknown-attribute] attributes-declarations-definitions.c:58: Warning:
Unknown attribute: e_
[kernel] attributes-declarations-definitions.c:62: User Error:
unsupported attribute: vector_size
[kernel] User Error: stopping on file "attributes-declarations-definitions.c" that has errors. Add
......
[kernel] Parsing osx_attribute.i (no preprocessing)
[kernel:unknown-attribute] osx_attribute.i:1: Warning:
Unknown attribute: availability
/* Generated by Frama-C */
void f(void) __attribute__((__availability__(macos,introduced=10.4,deprecated=10.6,obsoleted=10.7)));
......
[kernel] Parsing const_typedef.i (no preprocessing)
[kernel:unknown-attribute] const_typedef.i:9: Warning: Unknown attribute: BLA
[kernel:unknown-attribute] const_typedef.i:10: Warning: Unknown attribute: BLA
[kernel:unknown-attribute] const_typedef.i:11: Warning: Unknown attribute: BLA
[kernel:unknown-attribute] const_typedef.i:12: Warning: Unknown attribute: BLA
[kernel:unknown-attribute] const_typedef.i:19: Warning: Unknown attribute: BLA
/* Generated by Frama-C */
typedef int INT[3][3];
typedef int INT3[2][7];
......
[kernel] Parsing period.c (with preprocessing)
[kernel:unknown-attribute] period.c:4: Warning:
Unknown attribute: Frama_C_periodic
[kernel:unknown-attribute] period.c:13: Warning:
Unknown attribute: Frama_C_periodic
[kernel:unknown-attribute] period.c:14: Warning:
Unknown attribute: Frama_C_periodic
[kernel:unknown-attribute] period.c:15: Warning:
Unknown attribute: Frama_C_periodic
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
......
88,92d87
96,100d95
< [eva:alarm] period.c:53: Warning:
< pointer downcast. assert (unsigned int)(&g) ≤ 2147483647;
< [eva:garbled-mix:write] period.c:53:
< Assigning imprecise value to p because of arithmetic operation on addresses.
< [eva:alarm] period.c:54: Warning: out of bounds read. assert \valid_read(p);
102,105d96
110,113d104
< period.c:53: arithmetic operation on addresses
< (read in 1 statement, propagated through 1 statement) garbled mix of &
< {g}
......
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