ice-tea / CPF-UNITS

check unit errors for C programs utilizing C Policy Framework
2 stars 0 forks source link

ocaml-3.08.2 configure failed #1

Open PythonShell opened 8 years ago

PythonShell commented 8 years ago

My env: xubuntu 12.04 the configure step failed when I do ./configure in ./build/ocaml-3.08.2/ It says:

Source-level replay debugger: supported
Additional libraries supported:
        unix str num dynlink bigarray systhreads threads
Configuration for the "num" library:
        target architecture ...... ia32 (asm level 2)
Configuration for the "graph" library:
        options for compiling .... 
        options for linking ...... not found
The "labltk" library: not supported

** Objective Caml configuration completed successfully **

username@localhost:~/CPF-UNITS/build/ocaml-3.08.2$ 
PythonShell commented 8 years ago

先把 build/util//.c 在目标机都重新编译下~

username@localhost:~/CPF-UNITS$ ./cpf-test test.C 
compiling unit2cpf
# 1 "./step1.c"# 1 "<built-in>"# 1 "<command-line>"# 1 "./step1.c"struct A{int a;};int num1 = 8; ___CPFAssume(UNITS,"@unit(num1) = $m");int main(){int num2 =10; ___CPFAssume(UNITS,"@unit(num2) = $km");struct A aA; ___CPFAssume(UNITS,"@unit(aA.a) = $km");if(num1 < num2){num1 += aA.a;}else{num2 += aA.a;}return 0;}int num1 = 8; ___CPFAssume(UNITS,"@unit(num1) = $m");
main (defined):
  calls:
  is called by:
Analyzing function main
./parseunits: line 12: ./util/stripcpf/stripcpf: cannot execute binary file
Reading structure definitions
Finished reading structure definitions
Generating verification tasks
./cpf-test: line 13: ./maude.linux64: cannot execute binary file
username@localhost:~/CPF-UNITS$ 
PythonShell commented 8 years ago

I tried to recompile build/util//.c and modify ./cpf-test using ./maude.linux instead of ./maude.linux64

after running ./cpf-test test.C The result is show as:

$ ./cpf-test test.C 
compiling unit2cpf
# 1 "./step1.c"# 1 "<built-in>"# 1 "<command-line>"# 1 "./step1.c"struct A{int a;};int num1 = 8; ___CPFAssume(UNITS,"@unit(num1) = $m");int main(){int num2 =10; ___CPFAssume(UNITS,"@unit(num2) = $km");struct A aA; ___CPFAssume(UNITS,"@unit(aA.a) = $km");if(num1 < num2){num1 += aA.a;}else{num2 += aA.a;}return 0;}int num1 = 8; ___CPFAssume(UNITS,"@unit(num1) = $m");
main (defined):
  calls:
  is called by:
Analyzing function main
Reading structure definitions
Finished reading structure definitions
Generating verification tasks
Generating task for main
Task generated.
             \||||||||||||||||||/
           --- Welcome to Maude ---
             /||||||||||||||||||\
        Maude 2.6 built: Dec  9 2010 18:40:31
        Copyright 1997-2010 SRI International
           Fri Nov 27 06:46:33 2015
Maude> Warning: sort declarations for constant empty do not have an unique least sort.
Warning: sort declarations for operator __ failed preregularity check on 1 out of 289 sort
    tuples. First such tuple is (TypeQualifier, TypeQualifier).
Warning: sort declarations for constant empty do not have an unique least sort.
Warning: sort declarations for operator _`,_ failed preregularity check on 1 out of 36 sort
    tuples. First such tuple is (Declarator, Declarator).
Warning: sort declarations for associative operator __ are non-associative on 2 out of 4913 sort
    triples. First such triple is (TypeQualifierList, TypeQualifier, TypeQualifier).
Warning: sort declarations for associative operator _`,_ are non-associative on 4 out of 216
    sort triples. First such triple is (StructDeclaratorList, Declarator, Declarator).
==========================================
reduce in CHECK-UNITS : check("main", 
#CPFLine 7 decl(int, did(n('num1))) decl(int, did(n('num2))) decl(struct n('A), did(n('aA))) {
#CPFLine 9 #CPFCheckpoint 
#CPFLine 9 (n('num1) = i(8)) ; 
#CPFLine 9 #CPFAssume(n('UNITS),@unit(n('num1)) = $m); 
#CPFLine 11 (n('num2) = i(10)) ; 
#CPFLine 11 #CPFAssume(n('UNITS),@unit(n('num2)) = $km); 
#CPFLine 12 #CPFAssume(n('UNITS),@unit(n('aA) . n('a)) = $km); 
#CPFLine 14 (if n('num1) < n('num2) {
#CPFLine 15 (n('num1) = (n('num1) + (n('aA) . n('a)))) ;} else {
#CPFLine 18 (n('num2) = (n('num2) + (n('aA) . n('a)))) ;}) 
#CPFLine 20 return i(0) ;}, struct n('A){sdwrap(int, did(n('a)))}) .
rewrites: 1648 in 28ms cpu (33ms real) (58855 rewrites/second)
result StringList: "Function main: ",
    "ERROR on line 14(1): Unit violation detected in less than operation, incompatible units.",
    "ERROR on line 15(1): Unit violation detected in addition operation, incompatible units.",
    "Environments created = 2"
Maude> Bye.

I wanna to know if it means cpf-units is build success?