Frama-C-discuss mailing list archives

benjamin.monate at trust-in-soft.com (Benjamin Monate) · Sat, 12 Apr 2014 07:07:33 +0000

Hi,
Nice hack : this is similar to the "cilly" perl script that is provided with Cil.
At TrustInSoft we provide tis-make to our customers: this command calls your build script (usually make) and collects all subsequent low level compilation and linking command. It outputs a fresh Makefile whose targets are all binaries produced by the normal compilation and whose rules invoke Frama-C with the proper preprocessing options for all source files this binary depends on.  We use the Linux Kernel, Apache and a lot of other large C programs as test bench for tis-make.
We do not distribute this tool as Open Source Software but we may take part in projects that need it and provide the generated Makefile.
Usually preprocessing the files is not the most difficult task in a large formal verification project anyway and many other productivity tools and extensions of Frama-C are needed: this is the kind of things we develop and package at TrustInSoft.

Hope this helps,
Benjamin Monate
TrustInSoft founder and CTO

> Le 12 avr. 2014 ? 06:15, "Steven Stewart-Gallus" <sstewartgallus00 at mylangara.bc.ca> a ?crit :
> 
> So, I hacked together a simple Python script that fakes being a C compiler to
> gather build information and output JSON.
> I have some simple utility code that feeds the data into the Frama-C analyser
> but it might be nice if Frama-C gained the ability to interpret some sort of
> structured format for interpreting the list of files and build flags directly.
> One problem that'd fix is that all the files are processed with the same build
> flags. However, giving Frama-C that capability wouldn't fix the problem for
> other tools that are also limited and it might be smarter for me to make a
> separate program for doing this task.
> The code currently lives at
> https://gitorious.org/linted/linted/source/df5e4b4b20259571014b604c61f6717dd5d8e465:scripts/json-cc
> .
> Others might find this code useful and I will probably make a new repository for
> it eventually.
> When I do fix up the code enough and make a repository I could probably put a
> note up on the wiki.
> 
> #! /usr/bin/env python3.2
> # Copyright 2014 Steven Stewart-Gallus
> #
> # Licensed under the Apache License, Version 2.0 (the "License");
> # you may not use this file except in compliance with the License.
> # You may obtain a copy of the License at
> #
> #     http://www.apache.org/licenses/LICENSE-2.0
> #
> # Unless required by applicable law or agreed to in writing, software
> # distributed under the License is distributed on an "AS IS" BASIS,
> # WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
> # See the License for the specific language governing permissions and
> # limitations under the License.
> import os
> import subprocess
> import sys
> import json
> 
> def go():
>    arguments = sys.argv[1:]
>    ii = 0
> 
>    files = []
>    output = None
>    linking = True
>    flags = []
>    makeflags = []
>    while True:
>        if ii == len(arguments):
>            break
> 
>        argument = arguments[ii]
> 
>        if argument == '-c':
>            linking = False
>        elif argument == '-o':
>            ii += 1
> 
>            if ii == len(arguments):
>                raise Exception('No argument for o given')
> 
>            output = arguments[ii]
>        elif argument == '-MF' or argument == '-MT':
>            makeflags.append(argument)
> 
>            ii += 1
> 
>            if ii == len(arguments):
>                raise Exception('No argument for -MF or -MT given')
> 
>            makeflags.append(arguments[ii])
>        elif argument.startswith('-M') or argument == '-E' or argument == '-C':
>            makeflags.append(argument)
>        elif argument.startswith('-'):
>            flags.append(argument)
>        else:
>            files.append(argument)
> 
>        ii += 1
> 
>    if len(makeflags) > 0:
>        subprocess.check_call(['gcc', '-E'] + makeflags + flags + arguments)
>        # Fall through
> 
>    if 0 == len(files):
>        raise Exception('Some files are needed!')
>    elif linking:
>        if output == None:
>            output = 'a.out'
> 
>        files_json = []
>        for afile in files:
>            if afile.endswith('.c'):
>                files_json.append(afile)
>            elif afile.endswith('.a'):
>                members = subprocess.check_output(['ar', 't',
> afile]).decode('utf-8').split()
>                for member in members:
>                    member_contents = subprocess.check_output(['ar', 'p', afile,
> member])
>                    files_json.append(json.loads(member_contents.decode('utf-8')))
>            else:
>                print(afile)
>                files_json.append(json.loads(open(afile, 'r').read()))
> 
>        with open(output, 'w') as outputfile:
>            outputfile.write(json.JSONEncoder().encode({
>                'flags': flags,
>                'files': files_json
>            }))
> 
>    else:
>        if 1 == len(files):
>            input_file = files[0]
> 
>            if output == None:
>                output = input_file.replace('.c', '.o')
> 
>            with open(output, 'w') as outputfile:
>                outputfile.write(json.JSONEncoder().encode({
>                    'flags': flags,
>                    'files': [input_file]
>                }))
>        else:
>            if output == None:
>                raise Exception('cannot specify -o with -c with multiple files')
> 
>            for input_file in files:
>                with open(input_file.replace('.c', '.o'), 'w') as outputfile:
>                    outputfile.write(json.JSONEncoder().encode({
>                        'flags': flags,
>                        'files': [input_file]
>                    }))
> 
> if __name__ == '__main__':
>    go()
> 
> 
> _______________________________________________
> 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

Frama-C-discuss mailing list archives

[Frama-c-discuss] Is support for running frama-c in the place of a C compiler being considered?