source: CIVL/include/impls/times.cvl@ 1aaefd4

main test-branch
Last change on this file since 1aaefd4 was ea777aa, checked in by Alex Wilton <awilton@…>, 3 years ago

Moved examples, include, build_default.properties, common.xml, and README out from dev.civl.com into the root of the repo.

git-svn-id: svn://vsl.cis.udel.edu/civl/trunk@5704 fb995dde-84ed-4084-dfe6-e5aef3e2452c

  • Property mode set to 100644
File size: 574 bytes
Line 
1/* CIVL implementation of sys/time.h */
2
3#ifndef __CIVL_SYSTIMES__
4#define __CIVL_SYSTIMES__
5
6#include<sys/times.h>
7#include<civlc.cvh>
8
9struct tms{
10 clock_t tms_utime;
11 clock_t tms_stime;
12 clock_t tms_cutime;
13 clock_t tms_cstime;
14};
15
16clock_t times(tms *timer) {
17 $abstract double _time(int count);
18 int time_count = $next_time_count();
19 double result = _time(time_count);
20
21 if (time_count > 0) {
22 $assume(result > _time(time_count-1));
23 } else {
24 $assume(result > 0);
25 }
26 if(timer != NULL){
27 *timer->tms_utime = result;
28 }
29 return result;
30}
31
32#endif
Note: See TracBrowser for help on using the repository browser.