search

kenmcmil / ivy

IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing and experimenting with automated proof techniques. In particular, IVy provides interactive visualization of automated proofs, and supports a use model in which the human protocol designer and the automated tool interact to expose errors and prove correctness.
Other
77 stars 24 forks source link

ivy_to_cpp should mangle classnames derived from filenames #49

Open dijkstracula opened 2 years ago

dijkstracula commented 2 years ago

At present, one can't compile, for instance, an ivy file named time.ivy:

(venv) ➜  accord_ivy git:(main) ✗ cat walltime.ivy
#lang ivy1.8

# Some functionality for timestamp operations.

include collections

global {
}

module foo = {
}

(venv) ➜  accord_ivy git:(main) ✗ ivyc target=test walltime.ivy
g++ -Wno-parentheses-equality  -std=c++11  -I /Users/ntaylor/code/ivy/ivy/include -L /Users/ntaylor/code/ivy/ivy/lib -Xlinker -rpath -Xlinker /Users/ntaylor/code/ivy/ivy/lib -I /Users/ntaylor/code/ivy/submodules/z3/src/api/python/z3/include -L /Users/ntaylor/code/ivy/submodules/z3/src/api/python/z3/lib -Xlinker -rpath -Xlinker /Users/ntaylor/code/ivy/submodules/z3/src/api/python/z3/lib -I /usr/local/opt/openssl/include -L /usr/local/opt/openssl/lib -Xlinker -rpath -Xlinker /usr/local/opt/openssl/lib -g -o walltime walltime.cpp -lz3 -pthread
ld: warning: directory not found for option '-L/usr/local/opt/openssl/lib'
(venv) ➜  accord_ivy git:(main) ✗
(venv) ➜  accord_ivy git:(main) ✗ cp walltime.ivy time.ivy
(venv) ➜  accord_ivy git:(main) ✗ ivyc target=test time.ivy
g++ -Wno-parentheses-equality  -std=c++11  -I /Users/ntaylor/code/ivy/ivy/include -L /Users/ntaylor/code/ivy/ivy/lib -Xlinker -rpath -Xlinker /Users/ntaylor/code/ivy/ivy/lib -I /Users/ntaylor/code/ivy/submodules/z3/src/api/python/z3/include -L /Users/ntaylor/code/ivy/submodules/z3/src/api/python/z3/lib -Xlinker -rpath -Xlinker /Users/ntaylor/code/ivy/submodules/z3/src/api/python/z3/lib -I /usr/local/opt/openssl/include -L /usr/local/opt/openssl/lib -Xlinker -rpath -Xlinker /usr/local/opt/openssl/lib -g -o time time.cpp -lz3 -pthread
time.cpp:32:9: error: must use 'class' tag to refer to type 'time' in this scope
typedef time ivy_class;
        ^
        class
/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/time.h:118:8: note: class 'time' is hidden by a non-type declaration of 'time' here
time_t time(time_t *);
       ^
time.cpp:193:27: error: must use 'class' tag to refer to type 'time' in this scope
    virtual bool generate(time& obj)=0;
                          ^
                          class
/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/time.h:118:8: note: class 'time' is hidden by a non-type declaration of 'time' here
time_t time(time_t *);
       ^
time.cpp:194:26: error: must use 'class' tag to refer to type 'time' in this scope
    virtual void execute(time& obj)=0;
                         ^
                         class
/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/time.h:118:8: note: class 'time' is hidden by a non-type declaration of 'time' here
time_t time(time_t *);
       ^
time.cpp:1291:14: error: must use 'class' tag to refer to type 'time' in this scope
    init_gen(time&);
             ^
             class
/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/time.h:118:8: note: class 'time' is hidden by a non-type declaration of 'time' here
time_t time(time_t *);
       ^
time.cpp:1292:19: error: must use 'class' tag to refer to type 'time' in this scope
    bool generate(time&);
                  ^
                  class
/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/time.h:118:8: note: class 'time' is hidden by a non-type declaration of 'time' here
time_t time(time_t *);
       ^
time.cpp:1293:18: error: must use 'class' tag to refer to type 'time' in this scope
    void execute(time&){}
                 ^
                 class
/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/time.h:118:8: note: class 'time' is hidden by a non-type declaration of 'time' here
time_t time(time_t *);
       ^
time.cpp:1295:20: error: must use 'class' tag to refer to type 'time' in this scope
init_gen::init_gen(time &obj){
                   ^
                   class
/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/time.h:118:8: note: class 'time' is hidden by a non-type declaration of 'time' here
time_t time(time_t *);
       ^
time.cpp:1301:25: error: must use 'class' tag to refer to type 'time' in this scope
bool init_gen::generate(time& obj) {
                        ^
                        class
/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/time.h:118:8: note: class 'time' is hidden by a non-type declaration of 'time' here
time_t time(time_t *);
       ^
8 errors generated.
(venv) ➜  accord_ivy git:(main) ✗