Questions tagged [frama-c]
Frama-C is an Open Source suite of tools dedicated to the analysis of C source code.
451
questions
1
vote
0
answers
65
views
Why WP with Z3 proves \false when access to struct field is defined?
I've written simple ACSL contract for two C functions:
struct S
{
int n;
};
/*@ axiomatic Block {
predicate isZero(int left) =
left == 0;
// Unused, but necessary for ...
1
vote
1
answer
98
views
Has Frama-C been verified?
I am curious as to whether Frama-C has been formally verified using Frama-C or another verification framework, since bugs in Frama-C could possibly result in bugs in programs verified by Frama-C going ...
1
vote
1
answer
46
views
IDEs / Workflows for Frama-C? (notably, for the WP plugin)
TL;DR: How do you guys use the WP plugin? (what front-ends, build tools, etc. do you use? What's your workflow?)
Frama-C ships with frama-c-gui, a GUI that helps developers navigate and analyze code ...
1
vote
1
answer
59
views
How to demonstrate prerequisites set by instantiate plugin with WP
When using the instantiate plugin with frama-c (version 27), I'm unable to prove a precondition set by this plugin using either eva or eva and wp plugins.
This very simple piece of code illustrates ...
2
votes
1
answer
67
views
Defining hardware "storage" for processing by Frama-C EVA
The general structure of the headers for STM32 peripherals inside CMSIS,
typedef struct {
__IO uint32 REGn;
// ...
} SOC_PER_TypeDef;
#define SOC_PER_BASE 0x40003000
#define ...
2
votes
2
answers
201
views
Error while installing libgnomecanvas in MacOS Ventura (Frama-C pre-requisite) using brew on terminal
I am trying to install Frama-C in MacOS Ventura, which has as pre-requisite the installation of libgnomecanvas, but I get an error when installing by using brew.
When I use
brew install libgnomecanvas ...
0
votes
0
answers
109
views
How to instruct WP not to analyze dead or unreachable code
When running the command frama-c test.c -rte -eva -eva-slevel 1 then -wp on the following piece of code, I got the following results :
Frama-c 24 : No errors
Frama-c 25/26 : Overflows in the ...
0
votes
0
answers
86
views
What is the command to display abstract syntax tree for a program using frama-c?
I am using frama-c version Phosphorus-20170501. I want to generate abstract syntax tree for the programs using Frama-C. I need to do research on the abstract syntax tree generated from a program using ...
0
votes
1
answer
79
views
Tracking chained usage in huge legacy C codebase with Frama-C
I have huge (65 mln. lines of C code) legacy codebase.
Need to track usage of single cpp numeric const (#define MAX_NUM 32) which is used to define a number of structs (struct a { ... int a[MAX_NUM]; ....
4
votes
1
answer
41
views
How to increase Frama-C's GUI font/text size?
When running frama-c-gui, I'd like to increase its font size (for a tutorial, class, demo, video, etc), to ensure the text is visible in a large room. How can I do it?
1
vote
1
answer
32
views
__e_acsl_assert is not getting added for all given assert in .i file
I am new to Frama-C. I specifically need to use e-acsl plugin for verification purposes. I used first.i file as
int main(void) {
int x = 0;
/∗@ assert x == 0; ∗/
/∗@ assert x == 1; ∗/
return 0;
}
...
1
vote
1
answer
63
views
Failed to verifying the occurrence of a value in an array with logic function
I tried to use Frama-c to prove the occurrence of true value in an array that is the same as a integer which used to record the number of true values. But the prove failed if I want to change some ...
0
votes
0
answers
103
views
How to formally verify correctness of vectorized C code (or Fortran)
I'm trying to use Frama-c but I want to use AVX instructions in some places. Noramlly you can enable them with gcc -mavx2. Is there something like this for Frama-C. If not, is there some better tool ...
1
vote
1
answer
111
views
Importing large programs in FramaC
I have just started learning FramaC for testing of IOT programs. Is there a way to analyse large programs such as IoT OS in Frama C efficiently? How to import single modules without compiling for ...
0
votes
2
answers
57
views
How do frama-c get CWE-ID?
I am using Frama-c for my research. How can I do to get CWE-ID from the results of Frama-C
[kernel:typing:implicit-function-declaration] 1v3/juliet_suite-c-cplus/CWE401_Memory_Leak__int64_t_calloc_08....
1
vote
1
answer
47
views
Frama-C: how to get the start line number and the location of starting character?
Now I have PdgTypes.Node.stmt, I just can use:
Format.printf "%a"
Printer.pp_location (Cil_datatype.Stmt.loc PdgTypes.Node.stmt)
to print the result like this:
mkdir.c:500
But I want the ...
0
votes
2
answers
73
views
How to use frama-c to obtain the associated statements and then print their location
Follow this question:
How can I map frama-c CLI code to the original c statement? And how can I find the documentation of the api of the frama-c?
I used the Ocaml code mentioned in the question(ran ...
1
vote
1
answer
71
views
A potential bug in the induction strategy of Frama-C 24.0
I am working on the following proof and the invariant result_val is proved with an induction strategy on i using begin as the base case.
The sup case is trying to prove true which holds trivially ...
0
votes
1
answer
132
views
Frama-C: Warning: Memory model hypotheses for function 'write'; What does it mean?
I am new to frama-c. I did some tutorials and would like to build a tiny real world application. I didn't get far, because I ran into a warning that bugs me.
This is the program I would like to verify:...
0
votes
1
answer
80
views
Failed to establish an invariant requiring the knowledge of the content of an array
I try to use Frama-C to prove the invariant below. With the precondition that the array clean has at least one "true" in the first half, the loop should terminate before the last iteration ...
2
votes
1
answer
45
views
How to specify variable bounds in a clean way?
/*@
requires 0 <= lb < N_LOG_BLOCKS && 0 <= lp < N_PAGE ;
requires ( 1 <= h_clean_counter + l_clean_counter <= N_PHY_BLOCKS );
requires 0 <= ...
1
vote
1
answer
136
views
How to assert that a point is unreachable?
For Frama-C and the WP plugin, how can a user assert that a point in a program is unreachable?
Looking for something like:
//@ assert \unreachable;
2
votes
2
answers
100
views
Why can small size of array be proved, but can't large one?
I tried to prove a example from frama-c-wp-tutorial
That example is at Sect.6.2.4, but I modified some code.
#include <stdio.h>
#include <stdlib.h>
#include <stdbool.h>
#define size ...
3
votes
1
answer
77
views
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:
/...
1
vote
1
answer
106
views
Assigns two dimensional array
I tried to verify a program with 2-D array and encountered a problem in the assigns clause.
On the sample code, I can prove the assigns clause in the function of init_2D_2.
But, I failed to prove the ...
1
vote
1
answer
91
views
Frama-C/E-ACSL Error including header files with wrapper script
I am trying to analyze my code using the E-ACSL wrapper script but am facing issues when trying to include header files. For demonstration, I am using the following code and an include directory with ...
0
votes
0
answers
99
views
FRAMA-C/WP Goals not being proved
I am trying to prove a simplified version of an example from the WP manual but I keep getting an error for one of the ensures clauses.
Here is my code:
/*@ requires \valid(a) && \valid(b);
@ ...
0
votes
1
answer
30
views
E-ACSL wrapper script not creating files
I am new to Frama-C and wanted to ask what could be causing this issue:
When I run the E-ACSL wrapper script on annotated code with no header files, the a.out.e-acsl file is properly created.
However, ...
1
vote
1
answer
80
views
How to include header files with E-ACSL wrapper script?
I am new to Frama-C and wanted to ask how I could add header files when using the E-ACSL wrapper script. Normally, I've been adding header files the following way with WP and RTE:
frama-c -rte main.c -...
1
vote
1
answer
50
views
Why is my ACSL contract failing on my copy function?
I'm new to ACSL and I tried to replicate the function contract of this copy function provided by "ACSL by Example" from the Fraunhofer Society. The Code below works perfectly and every goal ...
0
votes
1
answer
89
views
Frama-C: unexpected error with _Bool values
While working with Frama-C I discovered an issue which leads to an unexpected error. The following code snippet shows a minimal reproducer of the problem (simplified as far as possible).
_Bool ...
1
vote
0
answers
40
views
How to share the information of logic variable between environment and use?
I'm trying to generate some annotations for functions. I have succeeded in implementing a plugin that achieves this purpose, but the problem that I am facing is that when I run tests on my plugin, an ...
0
votes
1
answer
33
views
Eva is not providing alarms for a code illustrating CWE122
My goal is to analyze a code illustrating CWE122 that I found in the NIST database : https://samate.nist.gov/SARD/test-cases/234158/versions/2.0.0
I dont succeed in making the tool emit an alarm for ...
2
votes
1
answer
93
views
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 ...
1
vote
1
answer
112
views
Frama C EVA undefined behavior
I tried to analyse a code that I found on the JULIET test directory, from the sate6 reproduction, dealing with the CWE758. For many of them, the tool does not detect the error. The results are unsound,...
2
votes
1
answer
78
views
How do I declare a logic variable?
I have implemented the example code in chapter 4.17.7 in the Developer Manual.
The example is a copy visitor that adds an assertion for each division in the program, stating that the divisor is not ...
1
vote
0
answers
58
views
Order of logical AND operands and impact on dependencies
I came across a strange behavior of Frama-C and have a question about it.
More precisely, it is about dependencies that come from expressions with the logical AND (&&).
The following minimal ...
2
votes
1
answer
54
views
Why does WP care about main?
In the following minimal example (slightly altered from Allan Blanchard's excellent tutorial -- section 3.2.3.3 Side Effects):
int h = 42;
/*@
requires \valid(a) && \valid(b);
requires \...
2
votes
1
answer
281
views
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 ...
3
votes
1
answer
56
views
Is it possible to write the result of code transformations back to the original source files?
I would like to perform code transformations on multiple files and write the changes that result from these transformations back, ideally the original files. For example, I would like to add an if-...
1
vote
1
answer
95
views
Wrong dependency: Dependency from whole array when only one value is being used
I'm working with frama-c to make a dependency analysis of our code base and we have run into a situation that I have summarized in the following example.
We have a our entry point "runnable" ...
0
votes
1
answer
94
views
Frama-Clang: Invalid integer constant
While working with Frama-Clang, I ran into a problem.
The following code shows the problem broken down to the minimum:
const long long value = -1;
int main(){
return 0;
}
Running the Frama-C (...
1
vote
0
answers
323
views
Frama-C Error with unbound logic variable?
I'm trying to generate a proof for a function that allocates to a void pointer, but when I write \valid(a) Frama-C can't process it because it's an unbound logic variable
#include <stdlib.h>
/*@...
1
vote
1
answer
47
views
Why WP can't deduce "else" close?
I'm trying to write the specification for a function which takes 2 pointers to int and put the smaller value to the first pointer and the other to the second.
Here is the code and the specification:
/*...
1
vote
1
answer
203
views
Frama-C does not recognize valid memory access from bitwise-ANDed index
I am right-shifting an unsigned integer then &ing it with 0b111, so the resulting value must be in the range [0, 7].
When I use that value as an index into an array of length 8, Frama-C is not ...
0
votes
1
answer
76
views
Multiple function call, dependencies mix up
While working with Frama-C, i encountered some strange dependencies. These occur when functions are called multiple times and pointers are passed as parameters. The following code shows the problem ...
2
votes
1
answer
83
views
Frama-C: Array accesses with non-deterministic sizes
I have been trying to reason about a loop over a dinamically-allocated array with a non-deterministic size, but I haven't been able to convince Frama-C/Eva of the\validity of memory that is returned ...
1
vote
1
answer
38
views
Frama-C does not verify zeroing-array example from https://frama-c.com/html/acsl.html
The example in this question seems to work only for fixed-length arrays, however the similar code below from https://frama-c.com/html/acsl.html doesn't seem to pass. As soon as I change the code to be ...
1
vote
1
answer
138
views
Frama-C with Eva plugin - Unsupported ACSL construct
I am currently trying to evaluate a test suite with Frama-C and it's plugin Eva. To do this I run Frama-C with the following flags:
frama-c -eva -cpp-extra-args="-DINCLUDEMAIN -I .../<...
2
votes
1
answer
51
views
Does Frama-C catch the UB of reading uninitialised stack variables?
I'm exploring Frama-C and tried this example, which according to the manual (on page 83) should be Handled (CWE-457), and the RTE manual 2.7 (do ints have a trap representation? http://www.open-std....