ACSL (ANSI/ISO C Specification Language) is a specification language for C programs, used by tools such as Frama-C.
Questions tagged [acsl]
40 questions
3
votes
1 answer
How to know which parts of an ACSL predicate are failing?
I have an ACSL predicate that is ~37 lines long (the predicate returns whether the passed struct is in a valid state).
It is a series of conditions &&'d together.
When I assert the predicate:
//@ assert MyPredicate(myArg);
and the verification…
Costava
- 175
- 9
3
votes
2 answers
How do you tell Frama-C and Eva that an entry point's parameters are assumed valid?
Take the following C code example.
struct foo_t {
int bar;
};
int my_entry_point(const struct foo_t *foo) {
return foo->bar;
}
In our case, my_entry_point will be called from assembly, and *foo here must be assumed to always be…
Qix - MONICA WAS MISTREATED
- 14,451
- 16
- 82
- 145
3
votes
1 answer
ACSL Logic Struct Declarations Not Working as in Reference Manual
I would like to have a way to describe logic/spec level structs that include abstract lists. Example 2.2.7 on page 27 of the ACSL Reference Manual suggests that there is a
way to do this and it is as follows:
//@ type point = struct { real x;…
Andrew Ferraiuolo
- 47
- 4
3
votes
1 answer
ACSL proof of a function that checks if an array is sorted in increasing or decreasing order
I'm trying to prove the correctness of an function that checks if an array is sorted in increasing/decreasing order or not sorted. The behaviour is to return -1 if sorted in decreasing order, 1 if sorted in increasing order, of size 1, or containing…
Nanoboss
- 193
- 1
- 10
3
votes
1 answer
How do I debug ACSL in frama-c?
I'm trying to learn ACSL but am stumbling with trying to write a complete specification. My code
#include
#include
#define NUM_ELEMS (8)
/*@ requires expected != test;
@ requires \let n = NUM_ELEMS;
@ …
Yifan
- 4,867
- 5
- 25
- 24
3
votes
1 answer
ACSL specification for a possibly infinite C function
I am trying to specify the behavior of external functions, more precisely, their termination. The ACSL documentation says that the \terminates p; property specifies that if the predicate p holds, then the function is guaranteed to terminate, but…
Anne
- 1,270
- 6
- 15
2
votes
1 answer
Frama-C: Creating a ghost field in a non-ghost structure
My goal is to create a ghost field in a non-ghost structure. What I understand from the ACSL manual (v.1.17) is, that this is possible in ACSL:
If a structure has ghost fields, the sizeof of the structure is the same as the structure without ghost…
jobnz
- 398
- 3
- 10
2
votes
1 answer
Frama-C Prove While Loop with "/*@ ensures"
I am a newbie at Frama-C and I am trying to validate a C code. The code is very basic but somehow I can not validate it.
In summary, I am trying to prove If that function or loop has ever run. For that, I give a variable a value (4) in the…
Uğur B
- 31
- 4
2
votes
1 answer
How do I write an "is power of 2" predicate in ACSL?
My attempt to write an ACSL predicate to see if an integer is a power of 2 goes like this:
/*@
predicate positive_power_of_2 (integer i) =
i > 0 &&
(i == 1 || ((i & 1) == 0 && positive_power_of_2 (i >> 1)));
*/
However when I added some…
Rich
- 926
- 1
- 9
- 17
2
votes
1 answer
ACSL list example in the documentation generate a bad sounding warning
I tried the list example (Example 2.23 on page 37, in Section "Function Contracts") from the ACSL manual, but I hid the implementation of incr_list and changed the return type. Full source below.
struct list {
int hd;
struct list *next;
};
/*@…
Justus Adam
- 43
- 5
2
votes
1 answer
frama-c slicing plugin appears to discard used stack values
Problem description
I'm developing a frama-c plugin that uses the slicing plugin as a library to remove unused bits of automatically generated code. Unfortunately the slicing plugin drops a bunch of stack values, which are actually used. They are…
Justus Adam
- 43
- 5
2
votes
1 answer
frama-c / ACSL / WP : Cardinality of a set
I often use cardinality of sets in others formal specifications and I wondering if it was possible to use it in ACSL with WP frama-c plugin.
For example, it seems clearer to me to write
assumes card({*a, *b, *c}) == 3
rather than
assumes *a != *b…
no_name
- 295
- 1
- 2
- 14
2
votes
3 answers
sh.exe is preventing windows cmd move command from working
I am running an old application called ACSLX. It is trying to call a DOS move command, but because sh.exe is in my path, I am getting an error. sh.exe is part of Git and also RTools, both of which I have installed. As you can see it is simply trying…
Simon Woodward
- 1,946
- 1
- 16
- 24
2
votes
0 answers
Shall we write "assert" after each function call when a sequence of functions are called?
Let me start my question by this example:
void A (void)
{
B();
C();
D();
E();
... // function calls go on.
return;
}
Now let's add ACSL annotations to the code:
/*@
ensures PostConditionOfB();
ensures PostConditionOfC();
…
Rocolife
- 43
- 4
2
votes
1 answer
ACSL "assigns" annotation for inner structs and fields of C code
Suppose we have such a data structure:
#typedef struct
{
int C_Field;
}C;
#typedef struct
{
C B_Array[MAX_SIZE];
}B;
#typedef struct
{
B A_Array[MAX_SIZE];
}A;
It seems that Frama-C doesn’t assign a location for a field of a struct of type C in…
Rocolife
- 43
- 4