X-Git-Url: http://git.liburcu.org/?a=blobdiff_plain;f=contrib%2Ffsm_checker%2FFD_CHECK%2Ffd.sm;fp=contrib%2Ffsm_checker%2FFD_CHECK%2Ffd.sm;h=f8603b666934d24be8da889c48a2a106f7bf50bb;hb=e09e518ebf18d490dbeb72c6358968af7d05d675;hp=0000000000000000000000000000000000000000;hpb=58f53b56557577b64911d0e7a2bba3fbb521d71d;p=lttv.git

diff --git a/contrib/fsm_checker/FD_CHECK/fd.sm b/contrib/fsm_checker/FD_CHECK/fd.sm
new file mode 100755
index 00000000..f8603b66
--- /dev/null
+++ b/contrib/fsm_checker/FD_CHECK/fd.sm
@@ -0,0 +1,65 @@
+
+
+%start Map1::Start
+%class fd
+%header fd.h
+
+%map Map1
+%%
+//STATE		TRANSITION				END STATE	ACTION(S)
+
+Start
+{
+		fs_close(pid: int, fd: int)	
+			CloseState			
+			{save_args(pid, fd);}
+	
+	
+		process_exit(pid: int, i: int)
+			[my_process_exit(ctxt, pid) == 1]
+			ExitState
+			{destroy_scenario(i);}
+
+		Default	
+			Start	
+			{}
+
+}
+
+CloseState
+{
+	fs_read(pid: int, fd: int, ts_sec: long, ts_nsec: long)
+		[test_args(ctxt,pid, fd) == 1]		
+		CloseState
+		{warning("Trying to read from a closed fd");print_ts(ts_sec, ts_nsec); skip_FSM();}
+	
+	fs_write(pid: int, fd: int)
+		[test_args(ctxt,pid, fd) == 1]		
+		CloseState
+		{warning("Trying to write to a closed fd");skip_FSM();}
+
+	process_exit(pid: int, i: int)
+		[my_process_exit(ctxt, pid) == 1]
+		ExitState
+		{destroy_scenario(i);}
+	
+	fs_open(pid: int, fd: int, i: int)
+		[test_args(ctxt, pid, fd)==1]
+		ExitState
+		{destroy_scenario(i);skip_FSM();}
+	
+	fs_dup3(pid: int, newfd: int, i: int)
+		[test_args(ctxt, pid, newfd)==1]
+		ExitState
+		{destroy_scenario(i);skip_FSM();}
+
+	Default CloseState {}
+}
+
+ExitState
+{
+	Default ExitState {}
+}
+
+%%
+