- Interprocedural Slicing Using Dependence Graphs
- Interprocedural Slicing Using Dependence Graphs presentation
- Exploring Frama-C to improve Assertion-based Slicing
- A Vocabulary of Program Slicing-Based Techniques
- Frama-C: A Software Analysis Perspective
- A Return Into the World of Static Analysis With Frama-C
- [Slides]Frama-C for Code Security
Slicing: Given a program P, slices are produced with respect to a given slicing criterion (S, V) which specifies a statement S and a set of variables V in P. The variables in V do not necesserily appears in S.
Backward Slicing: Slices the statements that could affect the criterion.
Forward Slicing: Slices the statements that are affected by the criterion.
Chopping: Slicing criterion selects two sets of variables source and sink. Slices all the statements in the program that being affected by source, affect sink. Generalization of forward and backward slicing where either source or sink is empty.
#include <stdio.h>
int f(void) {
return 5;
}
int main() {
int x, y;
x = 10;
y = 20;
x += f();
x += 5;
return x;
}
frama-c -metrics test.c
Output
[kernel] Parsing slice.c (with preprocessing)
[metrics] Defined functions (2)
=====================
f (1 call); main (0 call);
Undefined functions (0)
=======================
'Extern' global variables (0)
=============================
Potential entry points (1)
==========================
main;
Global metrics
==============
Sloc = 9
Decision point = 0
Global variables = 0
If = 0
Loop = 0
Goto = 0
Assignment = 6
Exit point = 2
Function = 2
Function call = 1
Pointer dereferencing = 0
Cyclomatic complexity = 2
frama-c test.c -slice-calls f -then-on 'Slicing export' -print
Output
#include "stddef.h"
#include "stdio.h"
int f_slice_1(void)
{
int __retres;
__retres = 5;
return __retres;
}
void main(void)
{
int tmp;
tmp = f_slice_1();
return;
}
Annotate the statement with //@ slicing pragma stmt; then frama-c test.c -slice-pragma main -then-on 'Slicing export' -print
Output of Test code 1 when sliced on return x statement.
/* Generated by Frama-C */
#include "stddef.h"
#include "stdio.h"
int f_slice_1(void)
{
int __retres;
__retres = 5;
return __retres;
}
int main(void)
{
int x;
int tmp;
x = 10;
tmp = f_slice_1();
x += tmp;
x += 5;
/*@ slice pragma stmt; */
return x;
}
Test code 2
#include <stdio.h>
int f(int x) {
int a = x, b = 0, c = 0;
a = a + 5;
b = a * b;
return b;
}
int main() {
int x, y, z;
x = 10;
y = 20;
z = 30;
y += f(z);
//@ slice pragma stmt;
x += 5;
x += f(1);
return y;
}
Output:
/* Generated by Frama-C */
#include "stddef.h"
#include "stdio.h"
void main(void)
{
int x;
x = 10;
/*@ slice pragma stmt; */
x += 5;
return;
}
Slice statements that affect a function's return statemnt.
frama-c slice.c -slice-return main,f -then-on 'Slicing export' -print
Test Code 3:
#include <stdio.h>
int f(void) {
int a = 0, b = 0, c = 0;
a = a + 5;
b = a * b;
return b;
}
int main() {
int x, y;
x = 10;
y = 20;
y += f();
x += 5;
return y;
}
Output:
/* Generated by Frama-C */
#include "stddef.h"
#include "stdio.h"
int f_slice_1(void)
{
int a = 0;
int b = 0;
a += 5;
b = a * b;
return b;
}
int main(void)
{
int y;
int tmp;
y = 20;
tmp = f_slice_1();
y += tmp;
return y;
}
Slice all the statements that are affected by a set of variables and affects the variables.
Test Code 4:
#include <stdio.h>
int f(int x) {
int a = x, b = 0, c = 0;
a = a + 5;
b = a * b;
return b;
}
int main() {
int x, y, z;
x = 10;
y = 20;
z = 30;
y += f(z);
//@ slice pragma stmt;
x += 5;
x += f(1);
return y;
}
Value slicing on test code 4 with respect to variable y: frama-c slice.c -slice-value y -then-on 'Slicing export' -print
Output:
/* Generated by Frama-C */
#include "stddef.h"
#include "stdio.h"
int f_slice_1(int x)
{
int a = x;
int b = 0;
a += 5;
b = a * b;
return b;
}
int main(void)
{
int y;
int z;
int tmp;
y = 20;
z = 30;
tmp = f_slice_1(z);
y += tmp;
return y;
}