roselone / pmgen Goto Github PK

Hello, I'm trying to install pmGen and use it to generate .pml from C files compiled. Maybe is a silly question but I cannot understand how to install it. Is there a tutorial to do this?

Kind regards

Hi @roselone. I am working at upgrading pmGen to work with llvm 5.0 and I am stuck on something. I know you haven't worked on this in a while, but I was hoping you would me able to answer a question of mine.

I noticed that the SlotTracker and the Helper classes are already classes in the llvm libraries (Helper is called AsmWriter in llvm). I was wondering why you made your own versions of them? Are you using the framework of AsmWriter and making it a PROMELA code writer? I am getting errors since a lot of the functions already exist:

g++ -fno-rtti -O0 -g -o bin/pmGen build/main.o build/IO.o build/TypeGen.o build/TypeFinder.o build/SlotTracker.o build/Helper.o '/home/build/llvm/bin/llvm-config --ldflags --libs --system-libs'

/home/build/llvm/lib/libLLVMCore.a(AsmWriter.cpp.o): In function 'llvm::SlotTracker::getLocalSlot(llvm::Value const*)': /home/llvm/lib/IR/AsmWriter.cpp:996: multiple definition of 'llvm::SlotTracker::getLocalSlot(llvm::Value const*)' build/SlotTracker.o:/home/pmGen/lib/Helper/SlotTracker.cpp:162: first defined here

/home/build/llvm/lib/libLLVMCore.a(AsmWriter.cpp.o): In function 'llvm::SlotTracker::getGlobalSlot(llvm::GlobalValue const*)': /home/llvm/lib/IR/AsmWriter.cpp:976: multiple definition of 'llvm::SlotTracker::getGlobalSlot(llvm::GlobalValue const*)' build/SlotTracker.o:/home/pmGen/lib/Helper/SlotTracker.cpp:142: first defined here

/home/build/llvm/lib/libLLVMCore.a(AsmWriter.cpp.o): In function 'llvm::SlotTracker::getMetadataSlot(llvm::MDNode const*)': /home/llvm/lib/IR/AsmWriter.cpp:986: multiple definition of 'llvm::SlotTracker::getMetadataSlot(llvm::MDNode const*)' build/SlotTracker.o:/home/pmGen/lib/Helper/SlotTracker.cpp:152: first defined here collect2: error: ld returned 1 exit status

make: *** [bin/pmGen] Error 1

Also I moved the SlotTracker code into its own header and .cpp files. I could probably figure out which flag is loading the AsmWriter lib, but I still have my question of why you made your own version of AsmWriter and SlotTracker. Thank you!

Hi would you please help me to implement your compiler, I want to use it, but I can't find how.
My request may be silly, but would you please help
Thank you