Frama-C-discuss mailing list archives

jean.nicolas at gmx.de (Jean-Pierre Nicolas) · Thu, 23 Sep 2010 09:05:51 +0200

For the "hello_world.ml" I get now this error on the terminal.

jean-pierre at jean-pierre-laptop:~/Bureau/ocamldoc$ make
/usr/share/frama-c/Makefile.dynamic:180: .depend: Aucun fichier ou dossier de ce type
ocamlc.opt -c  -I . -w Ael -warn-error A -annot   -g -I /usr/lib/frama-c  hello_world.ml
File "hello_world.ml", line 23, characters 4-35:
Error: This expression has type (unit -> unit) Type.t
       but an expression was expected of type (plugin:'a -> 'b) Type.t
make: *** [hello_world.cmo] Erreur 2

I've added the files "Makefile" and "hello_world.ml" to this mail.

Hello Julien,

Thanks for your answer. So if I've understood, it could be really difficult (perhaps impossible) to realise my destination (calculate the software complexity of a sourcecode written in C) with FRAMA-C.

Regards,
Jean-Pierre Nicolas

-------- Original-Nachricht --------
> Datum: Wed, 22 Sep 2010 15:33:14 +0200
> Von: Julien Signoles <Julien.Signoles at cea.fr>
> An: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr>
> Betreff: Re: [Frama-c-discuss] Calculation of SW complexity

> Hello,
> 
> Le 22/09/2010 14:47, Jean-Pierre Nicolas a ?crit :
> > Also if I've always got the problem to make the plugin 'hello_world', my
> interest is to make a plugin on FRAMA-C which analyse the sourcecode C and
> calculate the SW complexity:
> >
> > McCabe's Cyclomatic Complexity(MVG)
> > Halstead-Effort
> > Halstead-Volume
> > Halstead-Difficulty
> > Maintenance Index
> > Lines of Code(LOC)
> > Comment Lines (COM)
> 
> COM should be quite difficult to implement in Frama-C since this 
> platform does not keep comments in the AST, excepted the special ACSL
> ones.
> 
> > Fan-In, Fan-Out (FI,FIc,FIv,FO,FOc,FOv)
> 
> > Is it possible with FRAMA-C?
> 
> Even it is possible to implement pure syntactic static analysers as 
> Frama-C plug-ins, the main targets of Frama-C are semantic static 
> analysers. Within the last distributed version (Frama-C Boron), some 
> syntactic analyses are actually difficult to implement (or even 
> impossible without modifying the Frama-C kernel), since the original C 
> source code is syntactically modified by Frama-C itself in order to ease 
> the implementation of semantic analysers.
> 
> > To realise my calculation, I must know how i can make a plugin in
> FRAMA-C.
> 
> The so-called "Plug-in Development Guide" is what you need. It is freely 
> available from the Frama-C website:
> http://frama-c.com/download/plugin-developer-Boron-20100401.pdf.
> 
> > If I have understood correctly, I must write a sourcecode in OCaml for
> the calculation and also a Makefile to install the Ocaml-sourcecode in
> FRAMA-C.
> > But I don't know how a Makefile must be written.
> 
> No particular knowledge of make is required in order to write a Frama-C 
> plug-in Makefile. Mainly you just have to modify the Makefile of the 
> "Hello World" plug-in. Read the "Plug-in Development Guide" for details.
> 
> > I've started to learn OCaml since 7 weeks. It's absolutely different
> than C or Java. This functional language isn't easy to learn. After searching
> I found a little programm which calculate some of the results under the
> terminal of Ubuntu.
> 
> The WWW contains plenty resources about OCaml.
> 
> If I change the code of the files and the Makefile, it would be possible 
> to make a plugin, wouldn't it?
> 
> You must know OCaml in order to write a Frama-C plug-in. But an OCaml 
> code must follow ad-hoc Frama-C idioms to be a valid Frama-C plug-in. 
> Explaining these idioms is the raison d'?tre of the Plug-in Development 
> Guide. Once again read it for details. But before, I copy-paste some 
> parts of its introduction:
> 
> "This guide does not introduce neither the use of Frama-C which is the 
> purpose of the user manual [4], nor the use of plug-ins which should be 
> introduced in separated and dedicated manuals. We assume that the reader 
> of this guide already reads the Frama-C user manual and knows the main 
> Frama-C concepts.
> [...]
> Frama-C is fully developed within the Objective Caml programming 
> language (aka OCaml) [11]. Motivations for this choice are given in a 
> Frama-C experience report [6]. However this guide does not provide any 
> introduction to this programming language: the World Wide Web
> already contains plenty resources for OCaml developers (for instance, 
> see http://caml.inria.fr/resources/doc/index.en.html for getting many 
> pointers)."
> 
> Hope this helps,
> Julien Signoles
> -- 
> Ing?nieur-Chercheur
> CEA LIST, Laboratoire de S?ret? des Logiciels
> point courrier 94, 91191 Gif-Sur-Yvette Cedex
> tel:(+33)1.69.08.82.98  fax:(+33)1.69.08.83.95  Julien.Signoles at cea.fr
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

-- 
GMX DSL SOMMER-SPECIAL: Surf & Phone Flat 16.000 f?r nur 19,99 Euro/mtl.!*
http://portal.gmx.net/de/go/dsl
-------------- next part --------------
# Example of Makefile for dynamic plugins
#########################################

FRAMAC_SHARE        :=$(shell frama-c.byte -print-path)
FRAMAC_LIBDIR       :=$(shell frama-c.byte -print-libpath)
PLUGIN_NAME         = Hello
PLUGIN_CMO          = hello_world
include $(FRAMAC_SHARE)/Makefile.dynamic
-------------- next part --------------
A non-text attachment was scrubbed...
Name: hello_world.ml
Type: application/octet-stream
Size: 547 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100923/195d81c5/attachment.obj>