Questions tagged [value-analysis]
10 questions
5
votes
1 answer
What is the meaning and purpose of "after" column in Frama-C EVA plugin
In the EVA tutorial, I found this screenshot: with an explanation:" The exact value that caused this is shown in column c5: -1. The C standard considers the left-shift of a negative number as undefined behavior. Because -1 is the only possible…
Thuy Nguyen
- 353
- 2
- 10
5
votes
1 answer
Use Frama-c to analyze a project with CMake build infrastructure
I need to use frama-c value analysis plug-in to analyze some projects. These projects use CMake build infrastructure as their build system.
I have used frama-c to analyze each file separately. This way, the information about the entry point will be…
Mehrnoosh EP
- 161
- 7
3
votes
2 answers
Frama-C Plugin development: Getting result of value-analysis
I am working on a Plugin for Frama-C, using the Value-analysis.
I simply want to print the state of the variables (values) after each statement (I think the solution is quiet easy, but I couldn't figure it out).
I got the current state with…
Thomas Böhm
- 1,456
- 1
- 15
- 27
2
votes
1 answer
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 SOC_PER ((SOC_PER_TypeDef *)…
artless noise
- 21,212
- 6
- 68
- 105
2
votes
1 answer
scanf not working as expected in Frama-C
In the program below, function dec uses scanf to read an arbitrary input from the user.
dec is called from main and depending on the input it returns 1 or 0 and accordingly an operation will be performed. However, the value analysis indicates that…
karan
- 67
- 4
2
votes
1 answer
Value analysis for high loop bounds
I am analysing a control program with the following structure:
unsigned int cnt=0;
unsigned int inc=3;
...
void main(){
int i;
int lim;
for(i=0;i<100000;i++)
{
f1();
....
lim = f2();
if(cnt < lim)
cnt += inc;
....
}
}
My aim is to…
Harald
- 21
- 1
2
votes
2 answers
Calculate the range of an input which results in satisfying a predicate
Lets say we have the following C code:
int my_main(int x){
if (x > 5){
x++;
if (x > 8){
x++;
if (x < 15){
//@(x >= 9 && x <= 14);
}
}
}
return 0;
}
I'd like…
Maor Veitsman
- 1,544
- 9
- 21
2
votes
2 answers
Why is code unreachable in Frama-C Value Analysis?
When running Frama-C value analysis with some benchmarks, e.g. susan in http://www.eecs.umich.edu/mibench/automotive.tar.gz, we noticed that a lot of blocks are considered dead code or unreachable. However, in practice, these code is executed as we…
user2544482
- 157
- 4
2
votes
1 answer
Modify Entity Framework template to include ReSharper value analysis attributes on entity properties
My entity data model contains information about what fields are nullable and non-nullable. However, the generated templates do not include this information.
Elsewhere in my code, I use JetBrains.Annotations to show where null values are permitted,…
Drew Noakes
- 300,895
- 165
- 679
- 742
0
votes
1 answer
Frama-C Plugin-Development: Getting the values of value analysis of different calls
I am developing a Frama-C-Plugin this should print the values of the variables after each statement.
In the Frama-C-Gui, in the tab Values, I can see the values of the analysis over the whole program, and after different function calls (with the…
Thomas Böhm
- 1,456
- 1
- 15
- 27