# Coqimp

**Repository Path**: os-interrupt-power/coqimp

## Basic Information

- **Project Name**: Coqimp
- **Description**: 负责ucos系统中断和权能部分的验证
- **Primary Language**: Unknown
- **License**: Not specified
- **Default Branch**: master
- **Homepage**: None
- **GVP Project**: No

## Statistics

- **Stars**: 0
- **Forks**: 0
- **Created**: 2023-10-23
- **Last Updated**: 2024-02-25

## Categories & Tags

**Categories**: Uncategorized

**Tags**: None

## README

# Build instructions

The order of building files is recorded in `_CoqProject`. Changes to this file should be pushed to the remote repository.

To produce make file from `CoqProject`, use:

```bash
coq_makefile -f _CoqProject -o CoqMakefile
```

To make, use:

```bash
make -f CoqMakefile
```

(if MinGW on Windows is used, name of the `make` program may be `mingw32-make`, etc)

On Windows, it is also necessary to manually remove the following lines from `CoqMakefile` after each change to `_CoqProject` (lines 409-413):

```make
@# Extension point
$(HIDE)if [ "$(COQMAKEFILE_VERSION)" != "$(COQ_VERSION)" ]; then\
  echo "W: This Makefile was generated by Coq $(COQMAKEFILE_VERSION)";\
  echo "W: while the current Coq version is $(COQ_VERSION)";\
fi
```

# Specification of API functions

## `abs_op.v`

### Internal functions (original ucos API)

| Coq definition | Function |
| -------------- | -------- |
| tmdlycode | Time delay |
| timeget | Time query |
| semacc | Semaphore accept |
| semcre | Semaphore create |
| sem_pend | Semaphore pend |
| sem_post | Semaphore post |
| sem_post_bin | Semaphore binary post |
| mutexacc | Mutex accept |
| mutexcre | Mutex create |
| mutexpend | Mutex pend |
| mutexpost | Mutex post |
| qacceptnew | Queue accept |
| qcre | Queue create |
| qdel | Queue delete |
| qpendnew | Queue pend |
| qpost | Queue post |
| qtimedpost | Queue timed post |
| qquerynew | Queue query |

### API functions for events (new API)

| Coq definition | Function |
| -------------- | -------- |
| semtrywait | Semaphore try wait |
| seminit | Semaphore init |
| seminitbin | Semaphore binary init |
| semdestroy | Semaphore destroy |
| semwait | Semaphore wait |
| semtimedwait | Semaphore timed wait |
| semsignal_new | Semaphore signal (post?) |
| semflush | Semaphore flush |
| semgetvalue | Semaphore get value |
| mutexattrinit | Mutex attribute init |
| mutexattrdestroy | Mutex attribute destroy |
| mutexattrsettype | Mutex attribute set type |
| mutexattrgettype | Mutex attribute get type |
| mutexattrsetprioceiling | Mutex attribute set priority ceiling |
| mutexattrgetprioceiling | Mutex attribute get priority ceiling |
| mutextrylock | Mutex try lock |
| mutex_init | Mutex init |
| mutex_destroy | Mutex destroy |
| mutex_lock | Mutex lock |
| mutextimedlock | Mutex timed lock |
| mutexunlock | Mutex unlock |
| mqcreate | Queue create |
| mqdelete | Queue delete |
| mqreceive | Queue receive |
| mqtimedreceive | Queue timed receive |
| mqsend | Queue send |
| mqgetinfo | Queue get info |

### Other functions

| Coq definition | Function |
| -------------- | -------- |
| tickisr_spec | Time-tick ISR |
| taskcrecode | Task create |
| taskdelcode | Task delete |
| userisr | User ISR |
| ipcisr | IPC ISR |
| enablepiccode | Enable PIC |
| disablepiccode | Disable PIC |
| unlockcode | Unlock interrupt |
| lockcode | Lock interrupt |
| exchandler_setcode | Set exception handler |
| unstall_handler_6678code | Uninstall handler (6678) |
| unstall_handler_6713code | Uninstall handler (6713) |
| install_handler_6713code | Install handler (6713) |
| install_handler_6678code | Install handler (6678) |

# Specification of internal functions

## `ifun_spec.v`

| Coq definition | Function |
| -------------- | -------- |
| OS_EventWaitListInit | Event wait list init |
| ~~OS_EventSearch~~ | ~~Event search~~ |
| OS_EventRemove | Event remove |
| OS_EventRemoveDel | Event remove del |
| OS_EventTO | Event timeout |
| OS_EventPostTO | Event post timeout |
| OS_EventTaskRdy | Event task ready |
| OS_EventTaskWait | Event task wait |
| OS_Sched | Scheduling |
| ~~OSIntExit~~ | ~~Exit interrupt~~ |
| ~~OS_PrioChange~~ | ~~Priority change~~ |
| OSTimeTick | Time tick |
| OS_TCBInit | Task control block init |
| OS_IsSomeMutexOwner | Check task is mutex owner |
| UserAddrCheck | User address check |
| OSIntEnter | Enter interrupt |
| OSIntExit | Exit interrupt |
| EXC_HANDLER | Exception handler |
| OSTaskSuspend | Task suspend |
| fnull | ?? |
| OSIpc | IPC |
| Interrupt_Init | Interrupt init |
| UserAddrCheckEvt | User address check event |
| UserAddrCheckCrit | User address check critical |
| getFreePos | get free position |
| OS_EventTaskPostRdy | Event task post ready |
| OS_EventTaskPostRdyDel | Event task post ready del |
| OS_EventTaskPostWait | Event task post wait |
| OSSemAccept | Semaphore accept |
| OSSemCreate | Semaphore create |
| OSSemDel | Semaphore delete |
| OSSemPend | Semaphore pend |
| OSSemPost | Semaphore post |
| OSSemPostBin | Semaphore binary post |
| OSMutexAccept | Mutex accept |
| OSMutexCreate | Mutex create |
| OSMutexDel | Mutex delete |
| OSMutexPend | Mutex pend |
| OSMutexPost | Mutex post |
| OSQAccept | Queue accept |
| OSQCreate | Queue create |
| OSQDel | Queue delete |
| OSQPend | Queue pend |
| OSQPost | Queue post |
| OSQTimedPost | Queue timed post |
| OSQQuery | Queue query |