Questions tagged [frama-c]

Frama-C is an Open Source suite of tools dedicated to the analysis of C source code.

Filter by
Sorted by
Tagged with
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 ...
ReMarxist's user avatar
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 ...
Aadithyaa Eeswaran's user avatar
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 ...
willardthor's user avatar
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 ...
baronju's user avatar
  • 13
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 ...
artless noise's user avatar
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 ...
DavidSanan's user avatar
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 ...
baronju's user avatar
  • 13
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 ...
Sreenu's user avatar
  • 1
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]; ....
AlecN's user avatar
  • 17
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?
anol's user avatar
  • 8,414
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; } ...
Amrutha Benny's user avatar
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 ...
蔡登瑞's user avatar
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 ...
alagris's user avatar
  • 1,914
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 ...
Nirnai Rai's user avatar
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....
Nguyen Huong's user avatar
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 ...
BaiQi's user avatar
  • 15
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 ...
BaiQi's user avatar
  • 15
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 ...
Yu-Fang Chen's user avatar
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:...
Cosinus's user avatar
  • 554
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 ...
Yu-Fang Chen's user avatar
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 <= ...
Yu-Fang Chen's user avatar
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;
Costava's user avatar
  • 185
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 ...
蔡登瑞's user avatar
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: /...
Costava's user avatar
  • 185
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 ...
蔡登瑞's user avatar
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 ...
sgjl's user avatar
  • 27
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); @ ...
sgjl's user avatar
  • 27
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, ...
sgjl's user avatar
  • 27
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 -...
sgjl's user avatar
  • 27
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 ...
Robin 's user avatar
  • 13
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 ...
Gruber's user avatar
  • 25
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 ...
Hovig's user avatar
  • 33
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 ...
thomas's user avatar
  • 11
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 ...
jobnz's user avatar
  • 398
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,...
thomas's user avatar
  • 11
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 ...
Hovig's user avatar
  • 33
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 ...
Gruber's user avatar
  • 25
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 \...
Stephen Gaito's user avatar
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 ...
Uğur B's user avatar
  • 31
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-...
jobnz's user avatar
  • 398
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" ...
Adrián 's user avatar
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 (...
Gruber's user avatar
  • 25
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> /*@...
Quixoto's user avatar
  • 11
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: /*...
Dorian's user avatar
  • 502
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 ...
Costava's user avatar
  • 185
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 ...
Gruber's user avatar
  • 25
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 ...
hpacheco's user avatar
  • 235
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 ...
Dhruv Makwana's user avatar
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 .../<...
Gerry's user avatar
  • 13
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....
Dhruv Makwana's user avatar

1
2 3 4 5
10