SYSTEM WARNING: 'session_name(): Cannot change session name when session is active' in '/home/gitlab-www/dokuwiki/inc/init.php' line 231

SYSTEM WARNING: 'session_set_cookie_params(): Cannot change session cookie parameters when session is active' in '/home/gitlab-www/dokuwiki/inc/init.php' line 232

mantis:frama-c:explicit_alignment_howto [Frama-C]

User Tools

  • Logged in as: anonymous (anonymous)
  • Log Out

Site Tools


mantis:frama-c:explicit_alignment_howto

Frama-C is only able at this point to verify that an address is aligned on a n-bytes boundary when this property results from both the base address being aligned on a n-bytes boundary and the offset being a multiple of n. For instance, it is able to conclude in this example, because the base address of p+12 is an int array, and therefore 4-bytes aligned:

int t[10];
char *p;
p = (char *) t;
* (int*) (p+12) = 42; /* p + 12 should really be aligned
                       on a 4-bytes boundary */
                       

It definitely will be unable to conclude in the example below, because the alignement property results from choosing an offset that compensates the possible misalignement of the base address, and this kind of relation between the alignment of the base address and the computed offset can not be represented in the memory model used by Frama-C's value analysis.

char t[80];
char *p;
p = (t + 7) & ~7;
* (int*) p = 42; /* p absolutely needs to be aligned 
                    on a 4-bytes boundary */

Please find below a more complete example. In this example, one would like to check that the pointer passed to function f is always 4-bytes aligned.

#ifdef USING_FRAMA_C_FOR_VERIFICATION
#include ".../share/builtin.h"

int Frama_C_is_base_aligned(void *, int); 
/* this should be in .../share/builtin.h but it is not as of version 20080502 */

void check_alignment(void *p, int n)
{
  int good_alignment = Frama_C_is_base_aligned(p, n) && Frama_C_offset(p) % n == 0;

  if (!good_alignment) Frama_C_show_each_alignment_warning(p,n);
}

#define CHECK_ALIGNMENT(P, N) check_alignment(P, N);

#else

#define CHECK_ALIGNMENT(P, N) 

#endif

int t[12]; 

char c[14]; 

struct S { int a; char b; } s[5]; 

int o1, o2, o3; 

int r1, r2, r3;

int b1, b2, b3;



struct S2 { int a; char b[10]; int c;} s2;

int os2a, os2b, os2c;

int o;


void f (char * p){
  CHECK_ALIGNMENT (p, 4)
  *(int*)p = 42;
}

void main(void) 
{ 

  int i; 

#ifdef USING_FRAMA_C_FOR_VERIFICATION
  i = Frama_C_interval(0, 10);
#else
  i = 5;
#endif

  o1 = Frama_C_offset(&t[i]); 
  r1 = o1 % 4 == 0;
  b1 = Frama_C_is_base_aligned(&t[i], 4);
  
  f(&t[i]);

  f(c + 3);

  o2 = Frama_C_offset(&c[i]); 

  r2 = o2 % 4 == 0;
  b2 = Frama_C_is_base_aligned(&c[i], 4);


  o3 = Frama_C_offset(&s[i].a); 

  r3 = o3 % 4 == 0;
  b3 = Frama_C_is_base_aligned(&s[i].a, 4);

  f(&s[i].a);

  os2a = Frama_C_offset(&s2.a);

  os2b = Frama_C_offset(&s2.b);

  f(&s2.b);
 
  os2c = Frama_C_offset(&s2.c);

  f(&s2.c);
}

Use the command line (please replace … by Frama-C's installation path everywhere):

.../bin/frama-c-gui -val .../share/builtin.c alignement_args_fonctions.c -cpp-command "gcc -C -E -I. -D USING_FRAMA_C_FOR_VERIFICATION"

You should be able to observe the values of variables o1, r1, b1, … and see if they correspond to your expectations. Besides, please note the following lines in the analysis log:

[values] computing for function f <-main
[values] called from alignement_args_fonctions.c:66
[values] computing for function check_alignment <-f <-main
[values] called from alignement_args_fonctions.c:45
Argument of Frama_C_show_each_alignment_warning: {{ &c + {3; } ;}}
Argument of Frama_C_show_each_alignment_warning: {4; }

This part of the log mean that the analyzer is not able to guarantee that the parameter for f is aligned when it is called from line 66 in the example (the resolved address that poses a problem, c_3, is also printed, in case that helps to track down the problem and attribute it to either a bug in the source or a lack of precision in the analyzer).

mantis/frama-c/explicit_alignment_howto.txt · Last modified: 2010/06/11 23:18 by administrator