Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] -metrics discrepency Boron/Nitrogen
  • From: der.herr at hofr.at (Nicholas Mc Guire)
  • Date: Mon, 14 May 2012 10:46:38 +0200
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