shmsoc2011qgtt

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision		 Previous revision
shmsoc2011qgtt [2011/07/14 15:00] – MateuszKocielskishmsoc2011qgtt [2017/09/18 14:03] (current) – Use local wiki LinkNames (remove absolute wiki urls) KubilayKocak
Line 99: Line 99:
 </code> </code>
  
-Automata above describes event of assigning z to field y of x structure and then abc invocation. Other functions could be declared inside automaton block and could be called from main as well as other functions. Following keywords could be used to build valid sequences of events:+Automata above describes event of assigning z to field y of x structure followed by abc invocation. Other functions could be declared inside automaton block and could be called from main as well as other functions. Following keywords could be used to build valid sequences of events:
  
   * either { X } or { Y } - X or Y sequences are valid   * either { X } or { Y } - X or Y sequences are valid
Line 118: Line 118:
   * field_assign,struct type,field - means that instrumenter should handle assignments to field of struct type.   * field_assign,struct type,field - means that instrumenter should handle assignments to field of struct type.
  
-Script kernel/tesla-clang could be used to invoke plugin.+Script kernel/tesla-clang can be used to invoke plugin.
  
 ===== Simple example ===== ===== Simple example =====
Line 309: Line 309:
  
   * https://socsvn.freebsd.org/socsvn/soc2011/shm/ - SVN repository, header files of libtesla are well commented: https://socsvn.freebsd.org/socsvn/soc2011/shm/TESLA/tesla/   * https://socsvn.freebsd.org/socsvn/soc2011/shm/ - SVN repository, header files of libtesla are well commented: https://socsvn.freebsd.org/socsvn/soc2011/shm/TESLA/tesla/
-  * http://wiki.freebsd.org/BuildingFreeBSDWithClang - builing world using llvm/clang toolkit+  * [[BuildingFreeBSDWithClang|Building FreeBSD (world) using llvm/clang toolkit]]
   * [[ShmSoc2011|GSoC 2011 TESLA]] - Testing temporal properties with Temporally Enhanced Security Logic Assertions (TESLA)   * [[ShmSoc2011|GSoC 2011 TESLA]] - Testing temporal properties with Temporally Enhanced Security Logic Assertions (TESLA)
   * http://www.tcs.hut.fi/Studies/T-79.231/2003/slides5.pdf - Notes on Temporal logic   * http://www.tcs.hut.fi/Studies/T-79.231/2003/slides5.pdf - Notes on Temporal logic
  
  • shmsoc2011qgtt.1310655657.txt.gz
  • Last modified: 2011/07/14 15:00
  • by MateuszKocielski