--- layout: fc_discuss_archives title: Message 34 from Frama-C-discuss on May 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] -metrics discrepency Boron/Nitrogen



HI !


 below is a small snippet of code that causes the -metrics in nitrogen to 
 claim the existence of a goto ? anyway the boron output and nitrogen output
 are quite different - any idea what could be causing this - can this be my
 nitrogen build that messed things up ? build from source seemed ok.

hofrat at debsrv:~/tmp/$ frama-c --version
Version: Nitrogen-20111001
...
hofrat at debsrv:/tmp$ frama-c -metrics f.c
[kernel] preprocessing with "gcc -C -E -I.  f.c"
[metrics] Syntactic metrics
          -----------------
          ** Defined functions (1):
           dnl_insert (0 call); 
          
          ** Undefined functions (0):
           
          
          ** Potential entry points (1):
           dnl_insert; 
          
          SLOC: 19
          Number of if statements: 4
          Number of assignments: 12
          Number of loops: 0
          Number of calls: 0
          Number of gotos: 1
          Number of pointer access: 8

hofrat at debian:/tmp$ frama-c -version
Version: Boron-20100401
...
hofrat at debian:/tmp$ frama-c -metrics f.c
[kernel] preprocessing with "gcc -C -E -I.  f.c"
[metrics] Metrics printed to file metrics.html
[metrics] Syntactic metrics
           Defined function (1):
             dnl_insert  (0 call); 
           Undefined functions (0):
             
           Potential entry points (1):
             dnl_insert; 
           SLOC: 18
           Number of if statements: 4
           Number of assignments: 13
           Number of loops: 0
           Number of calls: 0
           Number of gotos: 0
           Number of pointer access: 8

Source file that produces the above output:

#include <stdlib.h> 	/* NULL */
typedef struct dln
{
	struct dln *next;
	struct dln *prev;
} TNode;

typedef struct
{
	TNode *head;
	TNode *tail;
} NList;

enum{
	INVAL_RET,
	INVAL_PTR,
	AT_TAIL,
	IN_LIST
};

int dnl_insert 
(
	NList *pList,
	TNode *pPrev,
	TNode *pNode
)
{
	int retval=INVAL_RET;
	TNode *pNext;

	if (pList == NULL || pNode == NULL) {
			retval=INVAL_PTR;
	} else {
		if (pPrev == NULL) {
	   		pNext = pList->head;
			pList->head = pNode;
			retval=AT_TAIL;
		} else {
			pNext = pPrev->next;
			pPrev->next = pNode;
			retval=IN_LIST;
		}

		if (pNext == NULL) {
	   		pList->tail = pNode;
		} else {
			pNext->prev = pNode;
		}

		pNode->next = pNext;
		pNode->prev = pPrev;
	}
	return retval;
}

both systems are Debian 6.0.3 same GCC, only (intentional) difference is the frama-c version

thx!
hofrat